-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

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

-- | Instructions working on product types derived from Haskell ones.
module Michelson.Typed.Haskell.Instr.Product
  ( InstrGetFieldC
  , InstrSetFieldC
  , InstrConstructC
  , instrGetField
  , instrSetField
  , instrConstruct
  , instrConstructStack
  , instrDeconstruct
  , InstrDeconstructC

  , GetFieldType
  , ConstructorFieldTypes
  , ConstructorFieldNames
  , FieldConstructor (..)
  , CastFieldConstructors (..)
  ) where

import qualified Data.Kind as Kind
import Data.Vinyl.Core (Rec(..))
import GHC.Generics ((:*:)(..), (:+:)(..))
import qualified GHC.Generics as G
import GHC.TypeLits (ErrorMessage(..), Symbol, TypeError)
import Named ((:!), (:?), NamedF(..))

import Michelson.Text
import Michelson.Typed.Haskell.Instr.Helpers
import Michelson.Typed.Haskell.Value
import Michelson.Typed.Instr
import Util.Label (Label)
import Util.Named (NamedInner)
import Util.Type

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

-- | Result of field lookup - its type and path to it in
-- the tree.
data LookupNamedResult = LNR Kind.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 '(:!)' or '(:?)'.
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 :: Kind.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 :: Kind.Type -> Kind.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 "Ambigous 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.
instrGetField
  :: forall dt name st.
     InstrGetFieldC dt name
  => Label name -> Instr (ToT dt ': st) (ToT (GetFieldType dt name) ': st)
instrGetField :: Label name -> Instr (ToT dt : st) (ToT (GetFieldType dt name) : st)
instrGetField _ =
  forall (s :: [T]).
(GInstrGet
   name
   (Rep dt)
   (LnrBranch (GetNamed name dt))
   (GetFieldType dt name),
 GIsoValue (Rep dt)) =>
Instr (GValueType (Rep dt) : s) (ToT (GetFieldType dt name) : s)
forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
       (s :: [T]).
(GInstrGet name x path fieldTy, GIsoValue x) =>
Instr (GValueType x : s) (ToT fieldTy : s)
gInstrGetField @name @(G.Rep dt) @(LnrBranch (GetNamed name dt))
    @(GetFieldType dt name)

-- | 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 `instrGetField` 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 'instrAccess'.
class GIsoValue x =>
  GInstrGet
    (name :: Symbol)
    (x :: Kind.Type -> Kind.Type)
    (path :: Path)
    (fieldTy :: Kind.Type) where
  gInstrGetField
    :: GIsoValue x
    => Instr (GValueType x ': s) (ToT fieldTy ': s)

instance GInstrGet name x path f => GInstrGet name (G.M1 t i x) path f where
  gInstrGetField :: Instr (GValueType (M1 t i x) : s) (ToT f : s)
gInstrGetField = forall (s :: [T]).
(GInstrGet name x path f, GIsoValue x) =>
Instr (GValueType x : s) (ToT f : s)
forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
       (s :: [T]).
(GInstrGet name x path fieldTy, GIsoValue x) =>
Instr (GValueType x : s) (ToT fieldTy : s)
gInstrGetField @name @x @path @f

instance (IsoValue f, ToT f ~ ToT f') =>
         GInstrGet name (G.Rec0 f) '[] f' where
  gInstrGetField :: Instr (GValueType (Rec0 f) : s) (ToT f' : s)
gInstrGetField = Instr (GValueType (Rec0 f) : s) (ToT f' : s)
forall (s :: [T]). Instr s s
Nop

instance (GInstrGet name x path f, GIsoValue y) => GInstrGet name (x :*: y) ('L ': path) f where
  gInstrGetField :: Instr (GValueType (x :*: y) : s) (ToT f : s)
gInstrGetField = Instr ('TPair (GValueType x) (GValueType y) : s) (GValueType x : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : s)) =>
Instr i o
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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` forall (s :: [T]).
(GInstrGet name x path f, GIsoValue x) =>
Instr (GValueType x : s) (ToT f : s)
forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
       (s :: [T]).
(GInstrGet name x path fieldTy, GIsoValue x) =>
Instr (GValueType x : s) (ToT fieldTy : s)
gInstrGetField @name @x @path @f

instance (GInstrGet name y path f, GIsoValue x) => GInstrGet name (x :*: y) ('R ': path) f where
  gInstrGetField :: Instr (GValueType (x :*: y) : s) (ToT f : s)
gInstrGetField = Instr ('TPair (GValueType x) (GValueType y) : s) (GValueType y : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (b : s)) =>
Instr i o
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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` forall (s :: [T]).
(GInstrGet name y path f, GIsoValue y) =>
Instr (GValueType y : s) (ToT f : s)
forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
       (s :: [T]).
(GInstrGet name x path fieldTy, GIsoValue x) =>
Instr (GValueType x : s) (ToT fieldTy : s)
gInstrGetField @name @y @path @f

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

type MyType1 = ("int" :! Integer, "bytes" :! ByteString, "bytes2" :? ByteString)

_getIntInstr1 :: Instr (ToT MyType1 ': s) (ToT Integer ': s)
_getIntInstr1 :: Instr (ToT MyType1 : s) (ToT Integer : s)
_getIntInstr1 = Label "int"
-> Instr (ToT MyType1 : s) (ToT (GetFieldType MyType1 "int") : s)
forall dt (name :: Symbol) (st :: [T]).
InstrGetFieldC dt name =>
Label name -> Instr (ToT dt : st) (ToT (GetFieldType dt name) : st)
instrGetField @MyType1 IsLabel "int" (Label "int")
Label "int"
#int

_getTextInstr1 :: Instr (ToT MyType1 ': s) (ToT (Maybe ByteString) ': s)
_getTextInstr1 :: Instr (ToT MyType1 : s) (ToT (Maybe ByteString) : s)
_getTextInstr1 = Label "bytes2"
-> Instr
     (ToT MyType1 : s) (ToT (GetFieldType MyType1 "bytes2") : s)
forall dt (name :: Symbol) (st :: [T]).
InstrGetFieldC dt name =>
Label name -> Instr (ToT dt : st) (ToT (GetFieldType dt name) : st)
instrGetField @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
Value (ToT MyType2) -> MyType2
WellTypedToT MyType2 =>
(MyType2 -> Value (ToT MyType2))
-> (Value (ToT MyType2) -> MyType2) -> IsoValue 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)
$cp1IsoValue :: WellTypedToT MyType2
IsoValue)

_getIntInstr2 :: Instr (ToT MyType2 ': s) (ToT () ': s)
_getIntInstr2 :: Instr (ToT MyType2 : s) (ToT () : s)
_getIntInstr2 = Label "getUnit"
-> Instr
     (ToT MyType2 : s) (ToT (GetFieldType MyType2 "getUnit") : s)
forall dt (name :: Symbol) (st :: [T]).
InstrGetFieldC dt name =>
Label name -> Instr (ToT dt : st) (ToT (GetFieldType dt name) : st)
instrGetField @MyType2 IsLabel "getUnit" (Label "getUnit")
Label "getUnit"
#getUnit

_getIntInstr2' :: Instr (ToT MyType2 ': s) (ToT Integer ': s)
_getIntInstr2' :: Instr (ToT MyType2 : s) (ToT Integer : s)
_getIntInstr2' =
  Label "getMyType1"
-> Instr
     (ToT MyType2 : s) (ToT (GetFieldType MyType2 "getMyType1") : s)
forall dt (name :: Symbol) (st :: [T]).
InstrGetFieldC dt name =>
Label name -> Instr (ToT dt : st) (ToT (GetFieldType dt name) : st)
instrGetField @MyType2 IsLabel "getMyType1" (Label "getMyType1")
Label "getMyType1"
#getMyType1 Instr
  ('TPair
     ('TPair 'TInt 'TString)
     ('TPair 'TUnit ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes))))
     : s)
  ('TPair
     (GValueType
        (M1
           S
           ('MetaSel
              'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
           (Rec0 (NamedF Identity Integer "int"))))
     (GValueType
        (S1
           ('MetaSel
              'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
           (Rec0 (NamedF Identity ByteString "bytes"))
         :*: S1
               ('MetaSel
                  'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
               (Rec0 (NamedF Maybe ByteString "bytes2"))))
     : s)
-> Instr
     ('TPair
        (GValueType
           (M1
              S
              ('MetaSel
                 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
              (Rec0 (NamedF Identity Integer "int"))))
        (GValueType
           (S1
              ('MetaSel
                 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
              (Rec0 (NamedF Identity ByteString "bytes"))
            :*: S1
                  ('MetaSel
                     'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                  (Rec0 (NamedF Maybe ByteString "bytes2"))))
        : s)
     ('TInt : s)
-> Instr
     ('TPair
        ('TPair 'TInt 'TString)
        ('TPair 'TUnit ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes))))
        : s)
     ('TInt : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Label "int"
-> Instr (ToT MyType1 : s) (ToT (GetFieldType MyType1 "int") : s)
forall dt (name :: Symbol) (st :: [T]).
InstrGetFieldC dt name =>
Label name -> Instr (ToT dt : st) (ToT (GetFieldType dt name) : st)
instrGetField @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 :: Label name
-> Instr (ToT (GetFieldType dt name) : ToT dt : st) (ToT dt : st)
instrSetField _ =
  forall (s :: [T]).
GInstrSetField
  name
  (Rep dt)
  (LnrBranch (GetNamed name dt))
  (GetFieldType dt name) =>
Instr
  (ToT (GetFieldType dt name) : GValueType (Rep dt) : s)
  (GValueType (Rep dt) : s)
forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
       (s :: [T]).
GInstrSetField name x path fieldTy =>
Instr (ToT fieldTy : GValueType x : s) (GValueType x : s)
gInstrSetField @name @(G.Rep dt) @(LnrBranch (GetNamed name dt))
    @(GetFieldType dt name)

-- | 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 :: Kind.Type -> Kind.Type)
    (path :: Path)
    (fieldTy :: Kind.Type) where
  gInstrSetField
    :: Instr (ToT fieldTy ': GValueType x ': s) (GValueType x ': s)

instance GInstrSetField name x path f => GInstrSetField name (G.M1 t i x) path f where
  gInstrSetField :: Instr
  (ToT f : GValueType (M1 t i x) : s) (GValueType (M1 t i x) : s)
gInstrSetField = forall (s :: [T]).
GInstrSetField name x path f =>
Instr (ToT f : GValueType x : s) (GValueType x : s)
forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
       (s :: [T]).
GInstrSetField name x path fieldTy =>
Instr (ToT fieldTy : GValueType x : s) (GValueType x : s)
gInstrSetField @name @x @path @f

instance (IsoValue f, ToT f ~ ToT f') =>
         GInstrSetField name (G.Rec0 f) '[] f' where
  gInstrSetField :: Instr (ToT f' : GValueType (Rec0 f) : s) (GValueType (Rec0 f) : s)
gInstrSetField = Instr (ToT f' : s) s -> Instr (ToT f' : ToT f' : s) (ToT f' : s)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr (ToT f' : s) s
forall (a :: T) (s :: [T]). Instr (a : s) s
DROP

instance (GInstrSetField name x path f, GIsoValue y) => GInstrSetField name (x :*: y) ('L ': path) f where
  gInstrSetField :: Instr (ToT f : GValueType (x :*: y) : s) (GValueType (x :*: y) : s)
gInstrSetField =
    Instr
  ('TPair (GValueType x) (GValueType y) : s)
  (GValueType x : GValueType y : s)
-> Instr
     (ToT f : 'TPair (GValueType x) (GValueType y) : s)
     (ToT f : 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)
  ('TPair (GValueType x) (GValueType y)
     : 'TPair (GValueType x) (GValueType y) : s)
forall (a :: T) (a :: [T]). Instr (a : a) (a : a : a)
DUP Instr
  ('TPair (GValueType x) (GValueType y) : s)
  ('TPair (GValueType x) (GValueType y)
     : 'TPair (GValueType x) (GValueType y) : s)
-> Instr
     ('TPair (GValueType x) (GValueType y)
        : 'TPair (GValueType x) (GValueType y) : s)
     ('TPair (GValueType x) (GValueType y) : GValueType y : s)
-> Instr
     ('TPair (GValueType x) (GValueType y) : s)
     ('TPair (GValueType x) (GValueType y) : GValueType y : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr ('TPair (GValueType x) (GValueType y) : s) (GValueType y : s)
-> Instr
     ('TPair (GValueType x) (GValueType y)
        : 'TPair (GValueType x) (GValueType y) : s)
     ('TPair (GValueType x) (GValueType y) : 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 y : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (b : s)) =>
Instr i o
CDR Instr
  ('TPair (GValueType x) (GValueType y) : s)
  ('TPair (GValueType x) (GValueType y) : GValueType y : s)
-> Instr
     ('TPair (GValueType x) (GValueType y) : GValueType y : s)
     (GValueType x : GValueType y : s)
-> Instr
     ('TPair (GValueType x) (GValueType y) : s)
     (GValueType x : GValueType y : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr
  ('TPair (GValueType x) (GValueType y) : GValueType y : s)
  (GValueType x : GValueType y : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : s)) =>
Instr i o
CAR) Instr
  (ToT f : 'TPair (GValueType x) (GValueType y) : s)
  (ToT f : GValueType x : GValueType y : s)
-> Instr
     (ToT f : GValueType x : GValueType y : s)
     (GValueType x : GValueType y : s)
-> Instr
     (ToT f : 'TPair (GValueType x) (GValueType y) : s)
     (GValueType x : GValueType y : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq`
    forall (s :: [T]).
GInstrSetField name x path f =>
Instr (ToT f : GValueType x : s) (GValueType x : s)
forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
       (s :: [T]).
GInstrSetField name x path fieldTy =>
Instr (ToT fieldTy : GValueType x : s) (GValueType x : s)
gInstrSetField @name @x @path @f Instr
  (ToT f : 'TPair (GValueType x) (GValueType y) : s)
  (GValueType x : GValueType y : s)
-> Instr
     (GValueType x : GValueType y : s)
     ('TPair (GValueType x) (GValueType y) : s)
-> Instr
     (ToT f : 'TPair (GValueType x) (GValueType y) : s)
     ('TPair (GValueType x) (GValueType y) : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq`
    Instr
  (GValueType x : GValueType y : s)
  ('TPair (GValueType x) (GValueType y) : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ (a : b : s), o ~ ('TPair a b : s)) =>
Instr i o
PAIR

instance (GInstrSetField name y path f, GIsoValue x) => GInstrSetField name (x :*: y) ('R ': path) f where
  gInstrSetField :: Instr (ToT f : GValueType (x :*: y) : s) (GValueType (x :*: y) : s)
gInstrSetField =
    Instr
  ('TPair (GValueType x) (GValueType y) : s)
  (GValueType y : GValueType x : s)
-> Instr
     (ToT f : 'TPair (GValueType x) (GValueType y) : s)
     (ToT f : 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)
  ('TPair (GValueType x) (GValueType y)
     : 'TPair (GValueType x) (GValueType y) : s)
forall (a :: T) (a :: [T]). Instr (a : a) (a : a : a)
DUP Instr
  ('TPair (GValueType x) (GValueType y) : s)
  ('TPair (GValueType x) (GValueType y)
     : 'TPair (GValueType x) (GValueType y) : s)
-> Instr
     ('TPair (GValueType x) (GValueType y)
        : 'TPair (GValueType x) (GValueType y) : s)
     ('TPair (GValueType x) (GValueType y) : GValueType x : s)
-> Instr
     ('TPair (GValueType x) (GValueType y) : s)
     ('TPair (GValueType x) (GValueType y) : GValueType x : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr ('TPair (GValueType x) (GValueType y) : s) (GValueType x : s)
-> Instr
     ('TPair (GValueType x) (GValueType y)
        : 'TPair (GValueType x) (GValueType y) : s)
     ('TPair (GValueType x) (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 : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : s)) =>
Instr i o
CAR Instr
  ('TPair (GValueType x) (GValueType y) : s)
  ('TPair (GValueType x) (GValueType y) : GValueType x : s)
-> Instr
     ('TPair (GValueType x) (GValueType y) : GValueType x : s)
     (GValueType y : GValueType x : s)
-> Instr
     ('TPair (GValueType x) (GValueType y) : s)
     (GValueType y : GValueType x : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr
  ('TPair (GValueType x) (GValueType y) : GValueType x : s)
  (GValueType y : GValueType x : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (b : s)) =>
Instr i o
CDR) Instr
  (ToT f : 'TPair (GValueType x) (GValueType y) : s)
  (ToT f : GValueType y : GValueType x : s)
-> Instr
     (ToT f : GValueType y : GValueType x : s)
     (GValueType y : GValueType x : s)
-> Instr
     (ToT f : 'TPair (GValueType x) (GValueType y) : s)
     (GValueType y : GValueType x : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq`
    forall (s :: [T]).
GInstrSetField name y path f =>
Instr (ToT f : GValueType y : s) (GValueType y : s)
forall (name :: Symbol) (x :: * -> *) (path :: Path) fieldTy
       (s :: [T]).
GInstrSetField name x path fieldTy =>
Instr (ToT fieldTy : GValueType x : s) (GValueType x : s)
gInstrSetField @name @y @path @f Instr
  (ToT f : 'TPair (GValueType x) (GValueType y) : s)
  (GValueType y : GValueType x : s)
-> Instr
     (GValueType y : GValueType x : s) (GValueType x : GValueType y : s)
-> Instr
     (ToT f : 'TPair (GValueType x) (GValueType y) : s)
     (GValueType x : GValueType y : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`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
  (ToT f : 'TPair (GValueType x) (GValueType y) : s)
  (GValueType x : GValueType y : s)
-> Instr
     (GValueType x : GValueType y : s)
     ('TPair (GValueType x) (GValueType y) : s)
-> Instr
     (ToT f : 'TPair (GValueType x) (GValueType y) : s)
     ('TPair (GValueType x) (GValueType y) : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr
  (GValueType x : GValueType y : s)
  ('TPair (GValueType x) (GValueType y) : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ (a : b : s), o ~ ('TPair a b : s)) =>
Instr i o
PAIR

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

_setIntInstr1 :: Instr (ToT Integer ': ToT MyType2 ': s) (ToT MyType2 ': s)
_setIntInstr1 :: Instr (ToT Integer : ToT MyType2 : s) (ToT MyType2 : s)
_setIntInstr1 = Label "getInt"
-> Instr
     (ToT (GetFieldType MyType2 "getInt") : ToT MyType2 : s)
     (ToT MyType2 : s)
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 :: Kind.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 :: Rec (FieldConstructor st) '[] -> Rec (FieldConstructor st) '[]
castFieldConstructorsImpl 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 :: Rec (FieldConstructor st) (x : xs)
-> Rec (FieldConstructor st) (y : ys)
castFieldConstructorsImpl (FieldConstructor fctr :: Instr (ToTs' st) (ToT r : ToTs' st)
fctr :& xs :: 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)
:& (Rec (FieldConstructor st) xs -> Rec (FieldConstructor st) ys
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 :: Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> Instr st (ToT dt : st)
instrConstruct = forall (st :: [T]).
GInstrConstruct (Rep dt) =>
Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> Instr st (GValueType (Rep dt) : st)
forall (x :: * -> *) (st :: [T]).
GInstrConstruct x =>
Rec (FieldConstructor st) (GFieldTypes x)
-> Instr st (GValueType x : st)
gInstrConstruct @(G.Rep dt)

instrConstructStack
  :: forall dt stack st .
  ( InstrConstructC dt
  , stack ~ ToTs (ConstructorFieldTypes dt)
  , KnownList stack
  )
  => Instr (stack ++ st) (ToT dt ': st)
instrConstructStack :: Instr (stack ++ st) (ToT dt : st)
instrConstructStack =
  Proxy st
-> Instr stack '[GValueType (Rep dt)]
-> Instr (stack ++ st) ('[GValueType (Rep dt)] ++ st)
forall (a :: [T]) (b :: [T]) (s :: [T]).
(KnownList a, KnownList b) =>
Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
FrameInstr (Proxy st
forall k (t :: k). Proxy t
Proxy @st) (GInstrConstruct (Rep dt) =>
Instr (ToTs (GFieldTypes (Rep dt))) '[GValueType (Rep dt)]
forall (x :: * -> *).
GInstrConstruct x =>
Instr (ToTs (GFieldTypes x)) '[GValueType x]
gInstrConstructStack @(G.Rep dt))

-- | 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 GIsoValue x => GInstrConstruct (x :: Kind.Type -> Kind.Type) where
  type GFieldTypes x :: [Kind.Type]
  gInstrConstruct :: Rec (FieldConstructor st) (GFieldTypes x) -> Instr st (GValueType x ': st)
  gInstrConstructStack :: Instr (ToTs (GFieldTypes x)) '[GValueType x]

instance GInstrConstruct x => GInstrConstruct (G.M1 t i x) where
  type GFieldTypes (G.M1 t i x) = GFieldTypes x
  gInstrConstruct :: Rec (FieldConstructor st) (GFieldTypes (M1 t i x))
-> Instr st (GValueType (M1 t i x) : st)
gInstrConstruct = forall (st :: [T]).
GInstrConstruct x =>
Rec (FieldConstructor st) (GFieldTypes x)
-> Instr st (GValueType x : st)
forall (x :: * -> *) (st :: [T]).
GInstrConstruct x =>
Rec (FieldConstructor st) (GFieldTypes x)
-> Instr st (GValueType x : st)
gInstrConstruct @x
  gInstrConstructStack :: Instr (ToTs (GFieldTypes (M1 t i x))) '[GValueType (M1 t i x)]
gInstrConstructStack = GInstrConstruct x => Instr (ToTs (GFieldTypes x)) '[GValueType x]
forall (x :: * -> *).
GInstrConstruct x =>
Instr (ToTs (GFieldTypes x)) '[GValueType x]
gInstrConstructStack @x

instance ( GInstrConstruct x, GInstrConstruct y
         , RSplit (GFieldTypes x) (GFieldTypes y)
         , KnownList (ToTs (GFieldTypes x)), KnownList (ToTs (GFieldTypes y))
         , ToTs (GFieldTypes x) ++ ToTs (GFieldTypes y) ~ ToTs (GFieldTypes x ++ GFieldTypes y)
         ) => GInstrConstruct (x :*: y) where
  type GFieldTypes (x :*: y) = GFieldTypes x ++ GFieldTypes y
  gInstrConstruct :: Rec (FieldConstructor st) (GFieldTypes (x :*: y))
-> Instr st (GValueType (x :*: y) : st)
gInstrConstruct fs :: Rec (FieldConstructor st) (GFieldTypes (x :*: y))
fs =
    let (lfs :: Rec (FieldConstructor st) (GFieldTypes x)
lfs, rfs :: Rec (FieldConstructor st) (GFieldTypes y)
rfs) = Rec (FieldConstructor st) (GFieldTypes x ++ GFieldTypes y)
-> (Rec (FieldConstructor st) (GFieldTypes x),
    Rec (FieldConstructor st) (GFieldTypes y))
forall k (l :: [k]) (r :: [k]) (f :: k -> *).
RSplit l r =>
Rec f (l ++ r) -> (Rec f l, Rec f r)
rsplit Rec (FieldConstructor st) (GFieldTypes x ++ GFieldTypes y)
Rec (FieldConstructor st) (GFieldTypes (x :*: y))
fs
        linstr :: Instr st (GValueType x : st)
linstr = Rec (FieldConstructor st) (GFieldTypes x)
-> Instr st (GValueType x : st)
forall (x :: * -> *) (st :: [T]).
GInstrConstruct x =>
Rec (FieldConstructor st) (GFieldTypes x)
-> Instr st (GValueType x : st)
gInstrConstruct @x Rec (FieldConstructor st) (GFieldTypes x)
lfs
        rinstr :: Instr st (GValueType y : st)
rinstr = Rec (FieldConstructor st) (GFieldTypes y)
-> Instr st (GValueType y : st)
forall (x :: * -> *) (st :: [T]).
GInstrConstruct x =>
Rec (FieldConstructor st) (GFieldTypes x)
-> Instr st (GValueType x : st)
gInstrConstruct @y Rec (FieldConstructor st) (GFieldTypes y)
rfs
    in 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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr
  (GValueType x : GValueType y : st)
  ('TPair (GValueType x) (GValueType y) : st)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ (a : b : s), o ~ ('TPair a b : s)) =>
Instr i o
PAIR

  gInstrConstructStack :: Instr (ToTs (GFieldTypes (x :*: y))) '[GValueType (x :*: y)]
gInstrConstructStack =
    let linstr :: Instr (ToTs (GFieldTypes x)) '[GValueType x]
linstr = GInstrConstruct x => Instr (ToTs (GFieldTypes x)) '[GValueType x]
forall (x :: * -> *).
GInstrConstruct x =>
Instr (ToTs (GFieldTypes x)) '[GValueType x]
gInstrConstructStack @x
        rinstr :: Instr (ToTs (GFieldTypes y)) '[GValueType y]
rinstr = GInstrConstruct y => Instr (ToTs (GFieldTypes y)) '[GValueType y]
forall (x :: * -> *).
GInstrConstruct x =>
Instr (ToTs (GFieldTypes x)) '[GValueType x]
gInstrConstructStack @y
    in Proxy (ToTs (GFieldTypes y))
-> Instr (ToTs (GFieldTypes x)) '[GValueType x]
-> Instr
     (ToTs (GFieldTypes x) ++ ToTs (GFieldTypes y))
     ('[GValueType x] ++ ToTs (GFieldTypes y))
forall (a :: [T]) (b :: [T]) (s :: [T]).
(KnownList a, KnownList b) =>
Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
FrameInstr (Proxy (ToTs (GFieldTypes y))
forall k (t :: k). Proxy t
Proxy @(ToTs (GFieldTypes y))) Instr (ToTs (GFieldTypes x)) '[GValueType x]
linstr Instr
  (ToTs (GFieldTypes x ++ GFieldTypes y))
  (GValueType x : ToTs (GFieldTypes y))
-> Instr
     (GValueType x : ToTs (GFieldTypes y)) '[GValueType x, GValueType y]
-> Instr
     (ToTs (GFieldTypes x ++ GFieldTypes y))
     '[GValueType x, GValueType y]
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (ToTs (GFieldTypes y)) '[GValueType y]
-> Instr
     (GValueType x : ToTs (GFieldTypes y)) '[GValueType x, GValueType y]
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr (ToTs (GFieldTypes y)) '[GValueType y]
rinstr Instr
  (ToTs (GFieldTypes x ++ GFieldTypes y))
  '[GValueType x, GValueType y]
-> Instr
     '[GValueType x, GValueType y]
     '[ 'TPair (GValueType x) (GValueType y)]
-> Instr
     (ToTs (GFieldTypes x ++ GFieldTypes y))
     '[ 'TPair (GValueType x) (GValueType y)]
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr
  '[GValueType x, GValueType y]
  '[ 'TPair (GValueType x) (GValueType y)]
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ (a : b : s), o ~ ('TPair a b : s)) =>
Instr i o
PAIR

instance GInstrConstruct G.U1 where
  type GFieldTypes G.U1 = '[]
  gInstrConstruct :: Rec (FieldConstructor st) (GFieldTypes U1)
-> Instr st (GValueType U1 : st)
gInstrConstruct RNil = Instr st (GValueType U1 : st)
forall (s :: [T]). Instr s ('TUnit : s)
UNIT
  gInstrConstructStack :: Instr (ToTs (GFieldTypes U1)) '[GValueType U1]
gInstrConstructStack = Instr (ToTs (GFieldTypes U1)) '[GValueType U1]
forall (s :: [T]). Instr s ('TUnit : s)
UNIT

instance ( TypeError ('Text "Cannot construct sum type")
         , GIsoValue x, GIsoValue y
         ) => GInstrConstruct (x :+: y) where
  type GFieldTypes (x :+: y) = '[]
  gInstrConstruct :: Rec (FieldConstructor st) (GFieldTypes (x :+: y))
-> Instr st (GValueType (x :+: y) : st)
gInstrConstruct = Text
-> Rec (FieldConstructor st) '[]
-> Instr st ('TOr (GValueType x) (GValueType y) : st)
forall a. HasCallStack => Text -> a
error "impossible"
  gInstrConstructStack :: Instr (ToTs (GFieldTypes (x :+: y))) '[GValueType (x :+: y)]
gInstrConstructStack = Text -> Instr '[] '[ 'TOr (GValueType x) (GValueType y)]
forall a. HasCallStack => Text -> a
error "impossible"

instance IsoValue a => GInstrConstruct (G.Rec0 a) where
  type GFieldTypes (G.Rec0 a) = '[a]
  gInstrConstruct :: Rec (FieldConstructor st) (GFieldTypes (Rec0 a))
-> Instr st (GValueType (Rec0 a) : st)
gInstrConstruct (FieldConstructor i :: Instr (ToTs' st) (ToT r : ToTs' st)
i :& RNil) = Instr st (GValueType (Rec0 a) : st)
Instr (ToTs' st) (ToT r : ToTs' st)
i
  gInstrConstructStack :: Instr (ToTs (GFieldTypes (Rec0 a))) '[GValueType (Rec0 a)]
gInstrConstructStack = Instr (ToTs (GFieldTypes (Rec0 a))) '[GValueType (Rec0 a)]
forall (s :: [T]). Instr s s
Nop

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

_constructInstr1 :: Instr (ToT MyType1 ': s) (ToT MyType2 ': ToT MyType1 ': s)
_constructInstr1 :: Instr (ToT MyType1 : s) (ToT MyType2 : ToT MyType1 : s)
_constructInstr1 =
  forall (st :: [T]).
InstrConstructC MyType2 =>
Rec (FieldConstructor st) (ConstructorFieldTypes MyType2)
-> Instr st (ToT MyType2 : st)
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 (ToT MyType1 : s) (ToT MyType2 : ToT MyType1 : s))
-> Rec
     (FieldConstructor
        ('TPair 'TInt ('TPair 'TBytes ('TOption 'TBytes)) : 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 (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH (Integer -> Value (ToT Integer)
forall a. IsoValue a => a -> Value (ToT a)
toVal @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 (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH (MText -> Value (ToT MText)
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 (s :: [T]). Instr s ('TUnit : s)
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 (a :: T) (a :: [T]). Instr (a : a) (a : a : a)
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 :: Instr s (ToT MyType1 : s)
_constructInstr2 =
  forall (st :: [T]).
InstrConstructC MyType1 =>
Rec (FieldConstructor st) (ConstructorFieldTypes MyType1)
-> Instr st (ToT MyType1 : st)
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 (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH (Integer -> Value (ToT Integer)
forall a. IsoValue a => a -> Value (ToT a)
toVal @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 (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH (ByteString -> Value (ToT ByteString)
forall a. IsoValue a => a -> Value (ToT a)
toVal @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 (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH (Maybe ByteString -> Value (ToT (Maybe ByteString))
forall a. IsoValue a => a -> Value (ToT a)
toVal @(Maybe ByteString) (ByteString -> Maybe ByteString
forall a. a -> Maybe a
Just "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 = (GenericIsoValue dt, GInstrDeconstruct (G.Rep dt))

-- | For given complex type @dt@ deconstruct it to its field types.
instrDeconstruct
  :: forall dt stack st .
  (InstrDeconstructC dt
  , stack ~ ToTs (ConstructorFieldTypes dt)
  , KnownList stack
  )
  => Instr (ToT dt ': st) (stack ++ st)
instrDeconstruct :: Instr (ToT dt : st) (stack ++ st)
instrDeconstruct = Proxy st
-> Instr '[GValueType (Rep dt)] stack
-> Instr ('[GValueType (Rep dt)] ++ st) (stack ++ st)
forall (a :: [T]) (b :: [T]) (s :: [T]).
(KnownList a, KnownList b) =>
Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
FrameInstr (Proxy st
forall k (t :: k). Proxy t
Proxy @st) (Instr '[GValueType (Rep dt)] stack
 -> Instr (ToT dt : st) (stack ++ st))
-> Instr '[GValueType (Rep dt)] stack
-> Instr (ToT dt : st) (stack ++ st)
forall a b. (a -> b) -> a -> b
$ GInstrDeconstruct (Rep dt) =>
Instr '[GValueType (Rep dt)] (ToTs (GFieldTypes (Rep dt)))
forall (x :: * -> *).
GInstrDeconstruct x =>
Instr '[GValueType x] (ToTs (GFieldTypes x))
gInstrDeconstruct @(G.Rep dt)

-- | Generic traversal for 'instrDeconstruct'.
class GIsoValue x => GInstrDeconstruct (x :: Kind.Type -> Kind.Type) where
  gInstrDeconstruct :: Instr '[GValueType x] (ToTs (GFieldTypes x))

instance GInstrDeconstruct x => GInstrDeconstruct (G.M1 t i x) where
  gInstrDeconstruct :: Instr '[GValueType (M1 t i x)] (ToTs (GFieldTypes (M1 t i x)))
gInstrDeconstruct = GInstrDeconstruct x => Instr '[GValueType x] (ToTs (GFieldTypes x))
forall (x :: * -> *).
GInstrDeconstruct x =>
Instr '[GValueType x] (ToTs (GFieldTypes x))
gInstrDeconstruct @x

instance ( GInstrDeconstruct x, GInstrDeconstruct y
         , t ~ (x :*: y)
         , KnownList (ToTs (GFieldTypes x)), KnownList (ToTs (GFieldTypes y))
         , ToTs (GFieldTypes x) ++ ToTs (GFieldTypes y) ~ ToTs (GFieldTypes x ++ GFieldTypes y)
         ) => GInstrDeconstruct (x :*: y) where
  gInstrDeconstruct :: Instr '[GValueType (x :*: y)] (ToTs (GFieldTypes (x :*: y)))
gInstrDeconstruct =
    let linstr :: Instr '[GValueType x] (ToTs (GFieldTypes x))
linstr = GInstrDeconstruct x => Instr '[GValueType x] (ToTs (GFieldTypes x))
forall (x :: * -> *).
GInstrDeconstruct x =>
Instr '[GValueType x] (ToTs (GFieldTypes x))
gInstrDeconstruct @x
        rinstr :: Instr '[GValueType y] (ToTs (GFieldTypes y))
rinstr = GInstrDeconstruct y => Instr '[GValueType y] (ToTs (GFieldTypes y))
forall (x :: * -> *).
GInstrDeconstruct x =>
Instr '[GValueType x] (ToTs (GFieldTypes x))
gInstrDeconstruct @y
    in Instr
  '[ 'TPair (GValueType x) (GValueType y)]
  '[GValueType x, GValueType y]
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : b : s)) =>
Instr i o
UNPAIR Instr
  '[ 'TPair (GValueType x) (GValueType y)]
  '[GValueType x, GValueType y]
-> Instr
     '[GValueType x, GValueType y] (GValueType x : ToTs (GFieldTypes y))
-> Instr
     '[ 'TPair (GValueType x) (GValueType y)]
     (GValueType x : ToTs (GFieldTypes y))
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr '[GValueType y] (ToTs (GFieldTypes y))
-> Instr
     '[GValueType x, GValueType y] (GValueType x : ToTs (GFieldTypes y))
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr '[GValueType y] (ToTs (GFieldTypes y))
rinstr Instr
  '[ 'TPair (GValueType x) (GValueType y)]
  (GValueType x : ToTs (GFieldTypes y))
-> Instr
     (GValueType x : ToTs (GFieldTypes y))
     (ToTs (GFieldTypes x ++ GFieldTypes y))
-> Instr
     '[ 'TPair (GValueType x) (GValueType y)]
     (ToTs (GFieldTypes x ++ GFieldTypes y))
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Proxy (ToTs (GFieldTypes y))
-> Instr '[GValueType x] (ToTs (GFieldTypes x))
-> Instr
     ('[GValueType x] ++ ToTs (GFieldTypes y))
     (ToTs (GFieldTypes x) ++ ToTs (GFieldTypes y))
forall (a :: [T]) (b :: [T]) (s :: [T]).
(KnownList a, KnownList b) =>
Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
FrameInstr (Proxy (ToTs (GFieldTypes y))
forall k (t :: k). Proxy t
Proxy @(ToTs (GFieldTypes y))) Instr '[GValueType x] (ToTs (GFieldTypes x))
linstr

instance GInstrDeconstruct G.U1 where
  gInstrDeconstruct :: Instr '[GValueType U1] (ToTs (GFieldTypes U1))
gInstrDeconstruct = Instr '[GValueType U1] (ToTs (GFieldTypes U1))
forall (a :: T) (s :: [T]). Instr (a : s) s
DROP

instance ( TypeError ('Text "Cannot deconstruct sum type")
         , GIsoValue x, GIsoValue y
         ) => GInstrDeconstruct (x :+: y) where
  gInstrDeconstruct :: Instr '[GValueType (x :+: y)] (ToTs (GFieldTypes (x :+: y)))
gInstrDeconstruct = Text -> Instr '[ 'TOr (GValueType x) (GValueType y)] '[]
forall a. HasCallStack => Text -> a
error "impossible"

instance IsoValue a => GInstrDeconstruct (G.Rec0 a) where
  gInstrDeconstruct :: Instr '[GValueType (Rec0 a)] (ToTs (GFieldTypes (Rec0 a)))
gInstrDeconstruct = Instr '[GValueType (Rec0 a)] (ToTs (GFieldTypes (Rec0 a)))
forall (s :: [T]). Instr s s
Nop