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

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

-- | Instructions working on sum types derived from Haskell ones.
module Michelson.Typed.Haskell.Instr.Sum
  ( InstrWrapC
  , InstrWrapOneC
  , InstrCaseC
  , InstrUnwrapC
  , instrWrap
  , instrWrapOne
  , hsWrap
  , instrCase
  , (//->)
  , instrUnwrapUnsafe
  , hsUnwrap

  , CaseClauseParam (..)
  , CaseClause (..)
  , CaseClauses
  , GCaseClauses
  , GCaseBranchInput

  , Branch (..)
  , Path
  , CtorField (..)
  , ExtractCtorField
  , AppendCtorField
  , AppendCtorFieldAxiom
  , appendCtorFieldAxiom
  , GetCtorField
  , CtorHasOnlyField
  , CtorOnlyField
  , MyCompoundType

    -- * Helpers
  , IsPrimitiveValue
  ) where

import qualified Data.Kind as Kind
import Data.Singletons (SingI(..))
import Data.Type.Bool (type (||))
import Data.Vinyl.Core (Rec(..))
import GHC.Generics ((:*:)(..), (:+:)(..))
import qualified GHC.Generics as G
import GHC.TypeLits (AppendSymbol, ErrorMessage(..), Symbol, TypeError)
import Named ((:!), NamedF)
import Type.Reflection ((:~:)(Refl))
import Unsafe.Coerce (unsafeCoerce)

import Michelson.Text (MText, mt)
import Michelson.Typed.Entrypoints
import Michelson.Typed.Haskell.Instr.Helpers
import Michelson.Typed.Haskell.Value
import Michelson.Typed.Instr
import Michelson.Typed.T
import Michelson.Typed.Value
import Tezos.Address (Address)
import Tezos.Core (Mutez, Timestamp, ChainId)
import Tezos.Crypto (KeyHash, PublicKey, Signature)
import Util.Label (Label)
import Util.Type
import Util.TypeTuple

-- Constructors lookup (helper)
----------------------------------------------------------------------------

-- | We support only two scenarious - constructor with one field and
-- without fields. Nonetheless, it's not that sad since for sum types
-- we can't even assign names to fields if there are many (the style
-- guide prohibits partial records).
data CtorField
  = OneField Kind.Type
  | NoFields

-- | Get /something/ as field of the given constructor.
type family ExtractCtorField (cf :: CtorField) where
  ExtractCtorField ('OneField t) = t
  ExtractCtorField 'NoFields = ()

-- | Push field to stack, if any.
type family AppendCtorField (cf :: CtorField) (l :: [k]) :: [k] where
  AppendCtorField ('OneField t) (l :: [T]) = ToT t ': l
  AppendCtorField ('OneField t) (l :: [Kind.Type]) = t ': l
  AppendCtorField 'NoFields (l :: [T]) = l
  AppendCtorField 'NoFields (l :: [Kind.Type]) = l

-- | To use 'AppendCtorField' not only here for 'T'-based stacks, but also
-- later in Lorentz with 'Kind.Type'-based stacks we need the following property.
type AppendCtorFieldAxiom (cf :: CtorField) (st :: [Kind.Type]) =
  ToTs (AppendCtorField cf st) ~ AppendCtorField cf (ToTs st)

-- | Proof of 'AppendCtorFieldAxiom'.
appendCtorFieldAxiom
  :: ( AppendCtorFieldAxiom ('OneField Word) '[Int]
     , AppendCtorFieldAxiom 'NoFields '[Int]
     )
  => Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom :: Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom =
  -- In order to avoid a lot of boilerplate and burdening GHC type checker we
  -- write an unsafe code. Its correctness is tested in dummy constraints of
  -- this function.
  -- Alternative approach I compare this unsafe one with
  -- would be to implement @instance SingI@ for 'CtorField' and consider cases
  -- of 'CtorField' one by one, but this would require propagading
  -- @SingI (cf :: CtorField)@ constraint to all users of 'appendCtorFieldAxiom'.
  Dict ('[] ~ '[]) -> Dict (AppendCtorFieldAxiom cf st)
forall a b. a -> b
unsafeCoerce (Dict ('[] ~ '[]) -> Dict (AppendCtorFieldAxiom cf st))
-> Dict ('[] ~ '[]) -> Dict (AppendCtorFieldAxiom cf st)
forall a b. (a -> b) -> a -> b
$ AppendCtorFieldAxiom 'NoFields '[] =>
Dict (AppendCtorFieldAxiom 'NoFields '[])
forall (a :: Constraint). a => Dict a
Dict @(AppendCtorFieldAxiom 'NoFields '[])

-- | Result of constructor lookup - entry type and path to it in the tree.
data LookupNamedResult = LNR CtorField Path

type family LnrFieldType (lnr :: LookupNamedResult) where
  LnrFieldType ('LNR f _) = f
type family LnrBranch (lnr :: LookupNamedResult) :: Path where
  LnrBranch ('LNR _ p) = p

-- | Transitively find constructor of some sum type by its name.
--
-- Transitivity means that if sum type consists of other sum types,
-- they will be searched recursively.
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 (sub)constructor " ':<>: '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 ('G.MetaCons ctorName _ _) x) =
    -- This case corresponds to going straight into a data type (as
    -- opposed to going left or right when we encounter a sum type),
    -- so we need to prepend 'S' here if we successfully find a
    -- constructor.
    PrependS
    -- If we encounter a constructor with requested name, we consider
    -- search successful.
    (If (name == ctorName || name == ("c" `AppendSymbol` ctorName))
       ('Just $ 'LNR (GExtractFields x) '[])
        -- If we do not, we check whether we can go deeper (see
        -- description below).
        (If (GCanGoDeeper x)
        -- And here we essentially just recursively call this search.
        (GLookupNamedDeeper name x)
        -- Or return 'Nothing' if we can not go deeper.
         'Nothing
      )
    )
  GLookupNamed name (x :+: y) =
    LNMergeFound name (GLookupNamed name x) (GLookupNamed name y)
  GLookupNamed _ G.V1 = 'Nothing

-- Prepend 'S' to the path inside 'LookupNamedResult' (if 'Just' is passed).
-- Should be done in the case when we go straight into a data type.
type family PrependS (x :: Maybe LookupNamedResult) :: Maybe LookupNamedResult where
  PrependS 'Nothing = 'Nothing
  PrependS ('Just ('LNR cf path)) = 'Just ('LNR cf ('S ': path))

-- Helper type family to check whether we should search for a
-- constructor inside given data type which is supposed to be part of
-- another constructor. Basically we can go deeper only if we
-- encounter another ADT with a constructor storing at least something
-- and which is not a primitive type. We do not go deeper when we
-- encounter a product type here, because it means that there are multiple
-- fields inside one constructor (it is not supported).
type family GCanGoDeeper (x :: Kind.Type -> Kind.Type) :: Bool where
  GCanGoDeeper (_ :+: _) = 'True
  GCanGoDeeper (G.D1 _ x) = GCanGoDeeper x
  GCanGoDeeper (G.S1 _ (G.Rec0 x)) = CanGoDeeper x
  GCanGoDeeper (G.C1 _ _) = 'True
  GCanGoDeeper G.V1 = 'False
  GCanGoDeeper G.U1 = 'False
  GCanGoDeeper (_ :*: _) = 'False
  GCanGoDeeper x = TypeError
    ('Text "GCanGoDeeper encountered unexpected pattern: " ':<>: 'ShowType x)

-- | Whether given type represents an atomic Michelson value.
type family IsPrimitiveValue (x :: Kind.Type) :: Bool where
  IsPrimitiveValue (Maybe _) = 'True
  IsPrimitiveValue (NamedF _ _ _) = 'True
  IsPrimitiveValue Integer = 'True
  IsPrimitiveValue Natural = 'True
  IsPrimitiveValue Text = 'True
  IsPrimitiveValue MText = 'True
  IsPrimitiveValue Bool = 'True
  IsPrimitiveValue ByteString = 'True
  IsPrimitiveValue Mutez = 'True
  IsPrimitiveValue Address = 'True
  IsPrimitiveValue EpAddress = 'True
  IsPrimitiveValue KeyHash = 'True
  IsPrimitiveValue Timestamp = 'True
  IsPrimitiveValue PublicKey = 'True
  IsPrimitiveValue Signature = 'True
  IsPrimitiveValue (ContractRef _) = 'True
  IsPrimitiveValue (BigMap _ _) = 'True
  IsPrimitiveValue (Map _ _) = 'True
  IsPrimitiveValue (Set _) = 'True
  IsPrimitiveValue ([_]) = 'True
  IsPrimitiveValue (Operation' _) = 'True
  IsPrimitiveValue ChainId = 'True
  IsPrimitiveValue _ = 'False

-- Some types don't have Generic instances (e. g. primitives like Integer), so
-- we need another type family to handle them.
type CanGoDeeper (x :: Kind.Type) =
  If (IsPrimitiveValue x)
     'False
     (GCanGoDeeper (G.Rep x))

type family GLookupNamedDeeper (name :: Symbol) (x :: Kind.Type -> Kind.Type)
          :: Maybe LookupNamedResult where
  GLookupNamedDeeper name (G.S1 _ (G.Rec0 y))  = GLookupNamed name (G.Rep y)
  GLookupNamedDeeper name _ = TypeError
    ('Text "Attempt to go deeper failed while looking for sum type constructor"
     ':<>: 'ShowType name
     ':$$:
     'Text "Make sure that all constructors have exactly one field inside."
    )

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 constructor: " ':<>: 'ShowType name)

type family GExtractFields (x :: Kind.Type -> Kind.Type)
          :: CtorField where
  GExtractFields (G.S1 _ x) = GExtractFields x
  GExtractFields (G.Rec0 a) = 'OneField a
  GExtractFields G.U1 = 'NoFields
  GExtractFields (_ :*: _) = TypeError
    ('Text "Cannot automatically lookup constructors having multiple fields"
     ':$$:
     'Text "Consider using tuple instead")
    --- ^ @martoon: Probably we will have no use cases for such scenario
    --- anyway, tuples seem to be not worse than separate fields in most cases.

-- | Get type of constructor fields (one or zero) referred by given datatype
-- and name.
type GetCtorField dt ctor =
  LnrFieldType (GetNamed ctor dt)

-- | Expect referred constructor to have only one field (in form of constraint)
-- and extract its type.
type CtorHasOnlyField ctor dt f =
  GetCtorField dt ctor ~ 'OneField f

type family RequireOneField (ctor :: Symbol) (cf :: CtorField) :: Kind.Type where
  RequireOneField _ ('OneField f) = f
  RequireOneField ctor 'NoFields = TypeError
    ('Text "Expected exactly one field" ':$$:
     'Text "In constructor " ':<>: 'ShowType ctor)

-- | Expect referred constructor to have only one field
-- (otherwise compile error is raised) and extract its type.
type CtorOnlyField name dt =
  RequireOneField name (GetCtorField dt name)

----------------------------------------------------------------------------
-- Constructor wrapping instruction
----------------------------------------------------------------------------

-- | Wrap given element into a constructor with the given name.
--
-- Mentioned constructor must have only one field.
--
-- Since labels interpretable by "OverloadedLabels" extension cannot
-- start with capital latter, prepend constructor name with letter
-- "c" (see examples below).
instrWrap
  :: forall dt name st.
     InstrWrapC dt name
  => Label name
  -> Instr (AppendCtorField (GetCtorField dt name) st)
           (ToT dt ': st)
instrWrap :: Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap _ =
  forall (s :: [T]).
(GInstrWrap
   (Rep dt) (LnrBranch (GetNamed name dt)) (GetCtorField dt name),
 GIsoValue (Rep dt)) =>
Instr
  (AppendCtorField (GetCtorField dt name) s)
  (GValueType (Rep dt) : s)
forall (x :: * -> *) (path :: Path) (entryTy :: CtorField)
       (s :: [T]).
(GInstrWrap x path entryTy, GIsoValue x) =>
Instr (AppendCtorField entryTy s) (GValueType x : s)
gInstrWrap @(G.Rep dt) @(LnrBranch (GetNamed name dt))
                         @(LnrFieldType (GetNamed name dt))

-- | Like 'instrWrap' but only works for contructors with a single field.
-- Results in a type error if a constructor with no field is used instead.
instrWrapOne
  :: forall dt name st.
     InstrWrapOneC dt name
  => Label name
  -> Instr (ToT (CtorOnlyField name dt) ': st) (ToT dt ': st)
instrWrapOne :: Label name
-> Instr (ToT (CtorOnlyField name dt) : st) (ToT dt : st)
instrWrapOne _ =
  forall (s :: [T]).
(GInstrWrap
   (Rep dt)
   (LnrBranch (GetNamed name dt))
   (LnrFieldType (GetNamed name dt)),
 GIsoValue (Rep dt)) =>
Instr
  (AppendCtorField (LnrFieldType (GetNamed name dt)) s)
  (GValueType (Rep dt) : s)
forall (x :: * -> *) (path :: Path) (entryTy :: CtorField)
       (s :: [T]).
(GInstrWrap x path entryTy, GIsoValue x) =>
Instr (AppendCtorField entryTy s) (GValueType x : s)
gInstrWrap @(G.Rep dt) @(LnrBranch (GetNamed name dt))
                         @(LnrFieldType (GetNamed name dt))

type InstrWrapC dt name =
  ( GenericIsoValue dt
  , GInstrWrap (G.Rep dt)
      (LnrBranch (GetNamed name dt))
      (LnrFieldType (GetNamed name dt))
  )

type InstrWrapOneC dt name =
  ( InstrWrapC dt name
  , GetCtorField dt name ~ 'OneField (CtorOnlyField name dt)
  )

-- | Wrap a haskell value into a constructor with the given name.
--
-- This is symmetric to 'instrWrap'.
hsWrap
  :: forall dt name.
     InstrWrapC dt name
  => Label name
  -> ExtractCtorField (GetCtorField dt name)
  -> dt
hsWrap :: Label name -> ExtractCtorField (GetCtorField dt name) -> dt
hsWrap _ =
  Rep dt Any -> dt
forall a x. Generic a => Rep a x -> a
G.to (Rep dt Any -> dt)
-> (ExtractCtorField (GetCtorField dt name) -> Rep dt Any)
-> ExtractCtorField (GetCtorField dt name)
-> dt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p.
(GInstrWrap
   (Rep dt) (LnrBranch (GetNamed name dt)) (GetCtorField dt name),
 GIsoValue (Rep dt)) =>
ExtractCtorField (GetCtorField dt name) -> Rep dt p
forall (x :: * -> *) (path :: Path) (entryTy :: CtorField) p.
(GInstrWrap x path entryTy, GIsoValue x) =>
ExtractCtorField entryTy -> x p
gHsWrap @(G.Rep dt) @(LnrBranch (GetNamed name dt))
                             @(LnrFieldType (GetNamed name dt))

-- | Generic traversal for 'instrWrap'.
class GIsoValue x =>
  GInstrWrap
    (x :: Kind.Type -> Kind.Type)
    (path :: Path)
    (entryTy :: CtorField) where
  gInstrWrap
    :: GIsoValue x
    => Instr (AppendCtorField entryTy s) (GValueType x ': s)
  gHsWrap
    :: GIsoValue x
    => ExtractCtorField entryTy -> x p

instance GInstrWrap x path e => GInstrWrap (G.D1 i x) path e where
  gInstrWrap :: Instr (AppendCtorField e s) (GValueType (D1 i x) : s)
gInstrWrap = forall (s :: [T]).
(GInstrWrap x path e, GIsoValue x) =>
Instr (AppendCtorField e s) (GValueType x : s)
forall (x :: * -> *) (path :: Path) (entryTy :: CtorField)
       (s :: [T]).
(GInstrWrap x path entryTy, GIsoValue x) =>
Instr (AppendCtorField entryTy s) (GValueType x : s)
gInstrWrap @x @path @e
  gHsWrap :: ExtractCtorField e -> D1 i x p
gHsWrap = x p -> D1 i x p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (x p -> D1 i x p)
-> (ExtractCtorField e -> x p) -> ExtractCtorField e -> D1 i x p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p.
(GInstrWrap x path e, GIsoValue x) =>
ExtractCtorField e -> x p
forall (x :: * -> *) (path :: Path) (entryTy :: CtorField) p.
(GInstrWrap x path entryTy, GIsoValue x) =>
ExtractCtorField entryTy -> x p
gHsWrap @x @path @e

instance (GInstrWrap x path e, GIsoValue y, SingI (GValueType y)) =>
         GInstrWrap (x :+: y) ('L ': path) e where
  gInstrWrap :: Instr (AppendCtorField e s) (GValueType (x :+: y) : s)
gInstrWrap = forall (s :: [T]).
(GInstrWrap x path e, GIsoValue x) =>
Instr (AppendCtorField e s) (GValueType x : s)
forall (x :: * -> *) (path :: Path) (entryTy :: CtorField)
       (s :: [T]).
(GInstrWrap x path entryTy, GIsoValue x) =>
Instr (AppendCtorField entryTy s) (GValueType x : s)
gInstrWrap @x @path @e Instr (AppendCtorField e s) (GValueType x : s)
-> Instr
     (GValueType x : s) ('TOr (GValueType x) (GValueType y) : s)
-> Instr
     (AppendCtorField e s) ('TOr (GValueType x) (GValueType y) : s)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr (GValueType x : s) ('TOr (GValueType x) (GValueType y) : s)
forall (b :: T) (a :: T) (s :: [T]).
KnownT b =>
Instr (a : s) ('TOr a b : s)
LEFT
  gHsWrap :: ExtractCtorField e -> (:+:) x y p
gHsWrap = x p -> (:+:) x y p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
G.L1 (x p -> (:+:) x y p)
-> (ExtractCtorField e -> x p) -> ExtractCtorField e -> (:+:) x y p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p.
(GInstrWrap x path e, GIsoValue x) =>
ExtractCtorField e -> x p
forall (x :: * -> *) (path :: Path) (entryTy :: CtorField) p.
(GInstrWrap x path entryTy, GIsoValue x) =>
ExtractCtorField entryTy -> x p
gHsWrap @x @path @e

instance (GInstrWrap y path e, GIsoValue x, SingI (GValueType x)) =>
         GInstrWrap (x :+: y) ('R ': path) e where
  gInstrWrap :: Instr (AppendCtorField e s) (GValueType (x :+: y) : s)
gInstrWrap = forall (s :: [T]).
(GInstrWrap y path e, GIsoValue y) =>
Instr (AppendCtorField e s) (GValueType y : s)
forall (x :: * -> *) (path :: Path) (entryTy :: CtorField)
       (s :: [T]).
(GInstrWrap x path entryTy, GIsoValue x) =>
Instr (AppendCtorField entryTy s) (GValueType x : s)
gInstrWrap @y @path @e Instr (AppendCtorField e s) (GValueType y : s)
-> Instr
     (GValueType y : s) ('TOr (GValueType x) (GValueType y) : s)
-> Instr
     (AppendCtorField e s) ('TOr (GValueType x) (GValueType y) : s)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr (GValueType y : s) ('TOr (GValueType x) (GValueType y) : s)
forall (a :: T) (b :: T) (s :: [T]).
KnownT a =>
Instr (b : s) ('TOr a b : s)
RIGHT
  gHsWrap :: ExtractCtorField e -> (:+:) x y p
gHsWrap = y p -> (:+:) x y p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
G.R1 (y p -> (:+:) x y p)
-> (ExtractCtorField e -> y p) -> ExtractCtorField e -> (:+:) x y p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p.
(GInstrWrap y path e, GIsoValue y) =>
ExtractCtorField e -> y p
forall (x :: * -> *) (path :: Path) (entryTy :: CtorField) p.
(GInstrWrap x path entryTy, GIsoValue x) =>
ExtractCtorField entryTy -> x p
gHsWrap @y @path @e

instance (IsoValue e) =>
         GInstrWrap (G.C1 c (G.S1 i (G.Rec0 e))) '[ 'S] ('OneField e) where
  gInstrWrap :: Instr
  (AppendCtorField ('OneField e) s)
  (GValueType (C1 c (S1 i (Rec0 e))) : s)
gInstrWrap = Instr
  (AppendCtorField ('OneField e) s)
  (GValueType (C1 c (S1 i (Rec0 e))) : s)
forall (s :: [T]). Instr s s
Nop
  gHsWrap :: ExtractCtorField ('OneField e) -> C1 c (S1 i (Rec0 e)) p
gHsWrap = M1 S i (Rec0 e) p -> C1 c (S1 i (Rec0 e)) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (M1 S i (Rec0 e) p -> C1 c (S1 i (Rec0 e)) p)
-> (e -> M1 S i (Rec0 e) p) -> e -> C1 c (S1 i (Rec0 e)) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 R e p -> M1 S i (Rec0 e) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (K1 R e p -> M1 S i (Rec0 e) p)
-> (e -> K1 R e p) -> e -> M1 S i (Rec0 e) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> K1 R e p
forall k i c (p :: k). c -> K1 i c p
G.K1

-- This is the case when a sum type is part of another sum type.
-- Here 'sub' is intermediate sum type.
instance ( path ~ (x ': xs)
         , GInstrWrap (G.Rep sub) path e
         , GenericIsoValue sub
         , GIsoValue (G.Rep sub)
         ) =>
         GInstrWrap (G.C1 c (G.S1 i (G.Rec0 sub))) ('S ': x ': xs) e where
  gInstrWrap :: Instr
  (AppendCtorField e s) (GValueType (C1 c (S1 i (Rec0 sub))) : s)
gInstrWrap = forall (s :: [T]).
(GInstrWrap (Rep sub) path e, GIsoValue (Rep sub)) =>
Instr (AppendCtorField e s) (GValueType (Rep sub) : s)
forall (x :: * -> *) (path :: Path) (entryTy :: CtorField)
       (s :: [T]).
(GInstrWrap x path entryTy, GIsoValue x) =>
Instr (AppendCtorField entryTy s) (GValueType x : s)
gInstrWrap @(G.Rep sub) @path @e
  gHsWrap :: ExtractCtorField e -> C1 c (S1 i (Rec0 sub)) p
gHsWrap = M1 S i (Rec0 sub) p -> C1 c (S1 i (Rec0 sub)) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (M1 S i (Rec0 sub) p -> C1 c (S1 i (Rec0 sub)) p)
-> (ExtractCtorField e -> M1 S i (Rec0 sub) p)
-> ExtractCtorField e
-> C1 c (S1 i (Rec0 sub)) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 R sub p -> M1 S i (Rec0 sub) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (K1 R sub p -> M1 S i (Rec0 sub) p)
-> (ExtractCtorField e -> K1 R sub p)
-> ExtractCtorField e
-> M1 S i (Rec0 sub) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sub -> K1 R sub p
forall k i c (p :: k). c -> K1 i c p
G.K1 (sub -> K1 R sub p)
-> (ExtractCtorField e -> sub) -> ExtractCtorField e -> K1 R sub p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep sub Any -> sub
forall a x. Generic a => Rep a x -> a
G.to (Rep sub Any -> sub)
-> (ExtractCtorField e -> Rep sub Any) -> ExtractCtorField e -> sub
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p.
(GInstrWrap (Rep sub) path e, GIsoValue (Rep sub)) =>
ExtractCtorField e -> Rep sub p
forall (x :: * -> *) (path :: Path) (entryTy :: CtorField) p.
(GInstrWrap x path entryTy, GIsoValue x) =>
ExtractCtorField entryTy -> x p
gHsWrap @(G.Rep sub) @path @e

instance GInstrWrap (G.C1 c G.U1) '[ 'S] 'NoFields where
  gInstrWrap :: Instr (AppendCtorField 'NoFields s) (GValueType (C1 c U1) : s)
gInstrWrap = Value' Instr 'TUnit -> Instr s ('TUnit : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr 'TUnit
forall (instr :: [T] -> [T] -> *). Value' instr 'TUnit
VUnit
  gHsWrap :: ExtractCtorField 'NoFields -> C1 c U1 p
gHsWrap () = U1 p -> C1 c U1 p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 U1 p
forall k (p :: k). U1 p
G.U1

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

-- TODO [TM-186] Consider moving this stuff to test-suite using
-- doctest. Or at least add tests for correctness.

data MyType
  = MyCtor Integer
  | ComplexThing ()
  | UselessThing ("field1" :! ByteString, "field2" :! ())
  deriving stock (forall x. MyType -> Rep MyType x)
-> (forall x. Rep MyType x -> MyType) -> Generic MyType
forall x. Rep MyType x -> MyType
forall x. MyType -> Rep MyType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep MyType x -> MyType
$cfrom :: forall x. MyType -> Rep MyType x
Generic
  deriving anyclass WellTypedToT MyType
Value (ToT MyType) -> MyType
WellTypedToT MyType =>
(MyType -> Value (ToT MyType))
-> (Value (ToT MyType) -> MyType) -> IsoValue MyType
MyType -> Value (ToT MyType)
forall a.
WellTypedToT a =>
(a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
fromVal :: Value (ToT MyType) -> MyType
$cfromVal :: Value (ToT MyType) -> MyType
toVal :: MyType -> Value (ToT MyType)
$ctoVal :: MyType -> Value (ToT MyType)
$cp1IsoValue :: WellTypedToT MyType
IsoValue

_MyTypeMyCtor ::
  GetNamed "cMyCtor" MyType :~: 'LNR ('OneField Integer) '[ 'L, 'S]
_MyTypeMyCtor :: GetNamed "cMyCtor" MyType :~: 'LNR ('OneField Integer) '[ 'L, 'S]
_MyTypeMyCtor = GetNamed "cMyCtor" MyType :~: 'LNR ('OneField Integer) '[ 'L, 'S]
forall k (a :: k). a :~: a
Refl

_MyTypeComplexThing ::
  GetNamed "cComplexThing" MyType :~: 'LNR ('OneField ()) '[ 'R, 'L, 'S]
_MyTypeComplexThing :: GetNamed "cComplexThing" MyType
:~: 'LNR ('OneField ()) '[ 'R, 'L, 'S]
_MyTypeComplexThing = GetNamed "cComplexThing" MyType
:~: 'LNR ('OneField ()) '[ 'R, 'L, 'S]
forall k (a :: k). a :~: a
Refl

_wrapMyType1 :: Instr (ToT Integer ': s) (ToT MyType ': s)
_wrapMyType1 :: Instr (ToT Integer : s) (ToT MyType : s)
_wrapMyType1 = Label "cMyCtor"
-> Instr
     (AppendCtorField (GetCtorField MyType "cMyCtor") s)
     (ToT MyType : s)
forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyType IsLabel "cMyCtor" (Label "cMyCtor")
Label "cMyCtor"
#cMyCtor

-- If "c" prefix is too annoying, one can construct labels without
-- OverloadedLabels extension.
_wrapMyType1' :: Instr (ToT Integer ': s) (ToT MyType ': s)
_wrapMyType1' :: Instr (ToT Integer : s) (ToT MyType : s)
_wrapMyType1' = Label "MyCtor"
-> Instr
     (AppendCtorField (GetCtorField MyType "MyCtor") s) (ToT MyType : s)
forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyType @"MyCtor" Label "MyCtor"
forall (x :: Symbol) a. IsLabel x a => a
fromLabel

_wrapMyType2 :: Instr (ToT () ': s) (ToT MyType ': s)
_wrapMyType2 :: Instr (ToT () : s) (ToT MyType : s)
_wrapMyType2 = Label "cComplexThing"
-> Instr
     (AppendCtorField (GetCtorField MyType "cComplexThing") s)
     (ToT MyType : s)
forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyType IsLabel "cComplexThing" (Label "cComplexThing")
Label "cComplexThing"
#cComplexThing

_wrapMyType3 :: Instr (ToT (ByteString, ()) ': s) (ToT MyType ': s)
_wrapMyType3 :: Instr (ToT (ByteString, ()) : s) (ToT MyType : s)
_wrapMyType3 = Label "cUselessThing"
-> Instr
     (AppendCtorField (GetCtorField MyType "cUselessThing") s)
     (ToT MyType : s)
forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyType IsLabel "cUselessThing" (Label "cUselessThing")
Label "cUselessThing"
#cUselessThing

data MyType' = WrapBool Bool
  deriving stock (forall x. MyType' -> Rep MyType' x)
-> (forall x. Rep MyType' x -> MyType') -> Generic MyType'
forall x. Rep MyType' x -> MyType'
forall x. MyType' -> Rep MyType' x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep MyType' x -> MyType'
$cfrom :: forall x. MyType' -> Rep MyType' x
Generic
  deriving anyclass WellTypedToT MyType'
Value (ToT MyType') -> MyType'
WellTypedToT MyType' =>
(MyType' -> Value (ToT MyType'))
-> (Value (ToT MyType') -> MyType') -> IsoValue MyType'
MyType' -> Value (ToT MyType')
forall a.
WellTypedToT a =>
(a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
fromVal :: Value (ToT MyType') -> MyType'
$cfromVal :: Value (ToT MyType') -> MyType'
toVal :: MyType' -> Value (ToT MyType')
$ctoVal :: MyType' -> Value (ToT MyType')
$cp1IsoValue :: WellTypedToT MyType'
IsoValue

_MyType'WrapBool ::
  GetNamed "cWrapBool" MyType' :~: 'LNR ('OneField Bool) '[ 'S]
_MyType'WrapBool :: GetNamed "cWrapBool" MyType' :~: 'LNR ('OneField Bool) '[ 'S]
_MyType'WrapBool = GetNamed "cWrapBool" MyType' :~: 'LNR ('OneField Bool) '[ 'S]
forall k (a :: k). a :~: a
Refl

_wrapMyType' :: Instr (ToT Bool ': s) (ToT MyType' ': s)
_wrapMyType' :: Instr (ToT Bool : s) (ToT MyType' : s)
_wrapMyType' = Label "cWrapBool"
-> Instr
     (AppendCtorField (GetCtorField MyType' "cWrapBool") s)
     (ToT MyType' : s)
forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyType' IsLabel "cWrapBool" (Label "cWrapBool")
Label "cWrapBool"
#cWrapBool

data MyCompoundType
  = CompoundPart1 MyType
  | CompoundPart2 Integer
  | CompoundPart3 Address
  | CompoundPart4 MyType'
  deriving stock (forall x. MyCompoundType -> Rep MyCompoundType x)
-> (forall x. Rep MyCompoundType x -> MyCompoundType)
-> Generic MyCompoundType
forall x. Rep MyCompoundType x -> MyCompoundType
forall x. MyCompoundType -> Rep MyCompoundType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep MyCompoundType x -> MyCompoundType
$cfrom :: forall x. MyCompoundType -> Rep MyCompoundType x
Generic
  deriving anyclass WellTypedToT MyCompoundType
Value (ToT MyCompoundType) -> MyCompoundType
WellTypedToT MyCompoundType =>
(MyCompoundType -> Value (ToT MyCompoundType))
-> (Value (ToT MyCompoundType) -> MyCompoundType)
-> IsoValue MyCompoundType
MyCompoundType -> Value (ToT MyCompoundType)
forall a.
WellTypedToT a =>
(a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
fromVal :: Value (ToT MyCompoundType) -> MyCompoundType
$cfromVal :: Value (ToT MyCompoundType) -> MyCompoundType
toVal :: MyCompoundType -> Value (ToT MyCompoundType)
$ctoVal :: MyCompoundType -> Value (ToT MyCompoundType)
$cp1IsoValue :: WellTypedToT MyCompoundType
IsoValue

_MyCompoundTypeCompoundPart1 ::
  GetNamed "cCompoundPart1" MyCompoundType :~: 'LNR ('OneField MyType) '[ 'L, 'L, 'S]
_MyCompoundTypeCompoundPart1 :: GetNamed "cCompoundPart1" MyCompoundType
:~: 'LNR ('OneField MyType) '[ 'L, 'L, 'S]
_MyCompoundTypeCompoundPart1 = GetNamed "cCompoundPart1" MyCompoundType
:~: 'LNR ('OneField MyType) '[ 'L, 'L, 'S]
forall k (a :: k). a :~: a
Refl

_MyCompoundTypeMyCtor ::
  GetNamed "cMyCtor" MyCompoundType :~: 'LNR ('OneField Integer) '[ 'L, 'L, 'S, 'L, 'S]
_MyCompoundTypeMyCtor :: GetNamed "cMyCtor" MyCompoundType
:~: 'LNR ('OneField Integer) '[ 'L, 'L, 'S, 'L, 'S]
_MyCompoundTypeMyCtor = GetNamed "cMyCtor" MyCompoundType
:~: 'LNR ('OneField Integer) '[ 'L, 'L, 'S, 'L, 'S]
forall k (a :: k). a :~: a
Refl

_MyCompoundTypeCompoundPart2 ::
  GetNamed "cCompoundPart2" MyCompoundType :~: 'LNR ('OneField Integer) '[ 'L, 'R, 'S]
_MyCompoundTypeCompoundPart2 :: GetNamed "cCompoundPart2" MyCompoundType
:~: 'LNR ('OneField Integer) '[ 'L, 'R, 'S]
_MyCompoundTypeCompoundPart2 = GetNamed "cCompoundPart2" MyCompoundType
:~: 'LNR ('OneField Integer) '[ 'L, 'R, 'S]
forall k (a :: k). a :~: a
Refl

_MyCompoundTypeCompoundPart4 ::
  GetNamed "cCompoundPart4" MyCompoundType :~: 'LNR ('OneField MyType') '[ 'R, 'R, 'S]
_MyCompoundTypeCompoundPart4 :: GetNamed "cCompoundPart4" MyCompoundType
:~: 'LNR ('OneField MyType') '[ 'R, 'R, 'S]
_MyCompoundTypeCompoundPart4 = GetNamed "cCompoundPart4" MyCompoundType
:~: 'LNR ('OneField MyType') '[ 'R, 'R, 'S]
forall k (a :: k). a :~: a
Refl

_MyCompoundTypeWrapBool ::
  GetNamed "cWrapBool" MyCompoundType :~: 'LNR ('OneField Bool) '[ 'R, 'R, 'S, 'S]
_MyCompoundTypeWrapBool :: GetNamed "cWrapBool" MyCompoundType
:~: 'LNR ('OneField Bool) '[ 'R, 'R, 'S, 'S]
_MyCompoundTypeWrapBool = GetNamed "cWrapBool" MyCompoundType
:~: 'LNR ('OneField Bool) '[ 'R, 'R, 'S, 'S]
forall k (a :: k). a :~: a
Refl

_wrapMyCompoundType1 :: Instr (ToT Integer ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType1 :: Instr (ToT Integer : s) (ToT MyCompoundType : s)
_wrapMyCompoundType1 = Label "cMyCtor"
-> Instr
     (AppendCtorField (GetCtorField MyCompoundType "cMyCtor") s)
     (ToT MyCompoundType : s)
forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyCompoundType IsLabel "cMyCtor" (Label "cMyCtor")
Label "cMyCtor"
#cMyCtor

_wrapMyCompoundType2 :: Instr (ToT Integer ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType2 :: Instr (ToT Integer : s) (ToT MyCompoundType : s)
_wrapMyCompoundType2 = Label "cCompoundPart2"
-> Instr
     (AppendCtorField (GetCtorField MyCompoundType "cCompoundPart2") s)
     (ToT MyCompoundType : s)
forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyCompoundType IsLabel "cCompoundPart2" (Label "cCompoundPart2")
Label "cCompoundPart2"
#cCompoundPart2

_wrapMyCompoundType3 :: Instr (ToT Bool ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType3 :: Instr (ToT Bool : s) (ToT MyCompoundType : s)
_wrapMyCompoundType3 = Label "cWrapBool"
-> Instr
     (AppendCtorField (GetCtorField MyCompoundType "cWrapBool") s)
     (ToT MyCompoundType : s)
forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyCompoundType IsLabel "cWrapBool" (Label "cWrapBool")
Label "cWrapBool"
#cWrapBool

_wrapMyCompoundType4 :: Instr (ToT MyType' ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType4 :: Instr (ToT MyType' : s) (ToT MyCompoundType : s)
_wrapMyCompoundType4 = Label "cCompoundPart4"
-> Instr
     (AppendCtorField (GetCtorField MyCompoundType "cCompoundPart4") s)
     (ToT MyCompoundType : s)
forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyCompoundType IsLabel "cCompoundPart4" (Label "cCompoundPart4")
Label "cCompoundPart4"
#cCompoundPart4

data MyEnum = Case1 | Case2 | CaseN Integer | CaseDef
  deriving stock (forall x. MyEnum -> Rep MyEnum x)
-> (forall x. Rep MyEnum x -> MyEnum) -> Generic MyEnum
forall x. Rep MyEnum x -> MyEnum
forall x. MyEnum -> Rep MyEnum x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep MyEnum x -> MyEnum
$cfrom :: forall x. MyEnum -> Rep MyEnum x
Generic
  deriving anyclass WellTypedToT MyEnum
Value (ToT MyEnum) -> MyEnum
WellTypedToT MyEnum =>
(MyEnum -> Value (ToT MyEnum))
-> (Value (ToT MyEnum) -> MyEnum) -> IsoValue MyEnum
MyEnum -> Value (ToT MyEnum)
forall a.
WellTypedToT a =>
(a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
fromVal :: Value (ToT MyEnum) -> MyEnum
$cfromVal :: Value (ToT MyEnum) -> MyEnum
toVal :: MyEnum -> Value (ToT MyEnum)
$ctoVal :: MyEnum -> Value (ToT MyEnum)
$cp1IsoValue :: WellTypedToT MyEnum
IsoValue

_wrapMyEnum1 :: Instr s (ToT MyEnum ': s)
_wrapMyEnum1 :: Instr s (ToT MyEnum : s)
_wrapMyEnum1 = Label "cCase1"
-> Instr
     (AppendCtorField (GetCtorField MyEnum "cCase1") s) (ToT MyEnum : s)
forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyEnum IsLabel "cCase1" (Label "cCase1")
Label "cCase1"
#cCase1

_wrapMyEnum2 :: Instr (ToT Integer ': s) (ToT MyEnum ': s)
_wrapMyEnum2 :: Instr (ToT Integer : s) (ToT MyEnum : s)
_wrapMyEnum2 = Label "cCaseN"
-> Instr
     (AppendCtorField (GetCtorField MyEnum "cCaseN") s) (ToT MyEnum : s)
forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyEnum IsLabel "cCaseN" (Label "cCaseN")
Label "cCaseN"
#cCaseN

data MyTypeWithNamedField
  = MeaninglessCtor
  | CtorWithNamedField ("name" :! Natural)
  deriving stock (forall x. MyTypeWithNamedField -> Rep MyTypeWithNamedField x)
-> (forall x. Rep MyTypeWithNamedField x -> MyTypeWithNamedField)
-> Generic MyTypeWithNamedField
forall x. Rep MyTypeWithNamedField x -> MyTypeWithNamedField
forall x. MyTypeWithNamedField -> Rep MyTypeWithNamedField x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep MyTypeWithNamedField x -> MyTypeWithNamedField
$cfrom :: forall x. MyTypeWithNamedField -> Rep MyTypeWithNamedField x
Generic
  deriving anyclass WellTypedToT MyTypeWithNamedField
Value (ToT MyTypeWithNamedField) -> MyTypeWithNamedField
WellTypedToT MyTypeWithNamedField =>
(MyTypeWithNamedField -> Value (ToT MyTypeWithNamedField))
-> (Value (ToT MyTypeWithNamedField) -> MyTypeWithNamedField)
-> IsoValue MyTypeWithNamedField
MyTypeWithNamedField -> Value (ToT MyTypeWithNamedField)
forall a.
WellTypedToT a =>
(a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
fromVal :: Value (ToT MyTypeWithNamedField) -> MyTypeWithNamedField
$cfromVal :: Value (ToT MyTypeWithNamedField) -> MyTypeWithNamedField
toVal :: MyTypeWithNamedField -> Value (ToT MyTypeWithNamedField)
$ctoVal :: MyTypeWithNamedField -> Value (ToT MyTypeWithNamedField)
$cp1IsoValue :: WellTypedToT MyTypeWithNamedField
IsoValue

_accessMyTypeWithNamedField :: Instr (ToT Natural ': s) (ToT MyTypeWithNamedField ': s)
_accessMyTypeWithNamedField :: Instr (ToT Natural : s) (ToT MyTypeWithNamedField : s)
_accessMyTypeWithNamedField = Label "cCtorWithNamedField"
-> Instr
     (AppendCtorField
        (GetCtorField MyTypeWithNamedField "cCtorWithNamedField") s)
     (ToT MyTypeWithNamedField : s)
forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyTypeWithNamedField IsLabel "cCtorWithNamedField" (Label "cCtorWithNamedField")
Label "cCtorWithNamedField"
#cCtorWithNamedField

----------------------------------------------------------------------------
-- "case" instruction
----------------------------------------------------------------------------

-- | Pattern-match on the given datatype.
instrCase
  :: forall dt out inp.
     InstrCaseC dt
  => Rec (CaseClause inp out) (CaseClauses dt) -> RemFail Instr (ToT dt ': inp) out
instrCase :: Rec (CaseClause inp out) (CaseClauses dt)
-> RemFail Instr (ToT dt : inp) out
instrCase = forall (inp :: [T]) (out :: [T]).
(GInstrCase (Rep dt), GIsoValue (Rep dt)) =>
Rec (CaseClause inp out) (CaseClauses dt)
-> RemFail Instr (GValueType (Rep dt) : inp) out
forall (x :: * -> *) (inp :: [T]) (out :: [T]).
(GInstrCase x, GIsoValue x) =>
Rec (CaseClause inp out) (GCaseClauses x)
-> RemFail Instr (GValueType x : inp) out
gInstrCase @(G.Rep dt)

type InstrCaseC dt = (GenericIsoValue dt, GInstrCase (G.Rep dt))

-- | In what different case branches differ - related constructor name and
-- input stack type which the branch starts with.
data CaseClauseParam = CaseClauseParam Symbol CtorField

-- | Type information about single case clause.
data CaseClause (inp :: [T]) (out :: [T]) (param :: CaseClauseParam) where
  CaseClause
    :: RemFail Instr (AppendCtorField x inp) out
    -> CaseClause inp out ('CaseClauseParam ctor x)

-- | Lift an instruction to case clause.
--
-- You should write out constructor name corresponding to the clause
-- explicitly. Prefix constructor name with "c" letter, otherwise
-- your label will not be recognized by Haskell parser.
-- Passing constructor name can be circumvented but doing so is not recomended
-- as mentioning contructor name improves readability and allows avoiding
-- some mistakes.
(//->)
  :: Label ("c" `AppendSymbol` ctor)
  -> RemFail Instr (AppendCtorField x inp) out
  -> CaseClause inp out ('CaseClauseParam ctor x)
//-> :: Label (AppendSymbol "c" ctor)
-> RemFail Instr (AppendCtorField x inp) out
-> CaseClause inp out ('CaseClauseParam ctor x)
(//->) _ = RemFail Instr (AppendCtorField x inp) out
-> CaseClause inp out ('CaseClauseParam ctor x)
forall (x :: CtorField) (inp :: [T]) (out :: [T]) (ctor :: Symbol).
RemFail Instr (AppendCtorField x inp) out
-> CaseClause inp out ('CaseClauseParam ctor x)
CaseClause
infixr 8 //->

-- | List of 'CaseClauseParam's required to pattern match on the given type.
type CaseClauses a = GCaseClauses (G.Rep a)

-- | Generic traversal for 'instrWrap'.
class GIsoValue x => GInstrCase (x :: Kind.Type -> Kind.Type) where

  type GCaseClauses x :: [CaseClauseParam]

  gInstrCase
    :: GIsoValue x
    => Rec (CaseClause inp out) (GCaseClauses x) -> RemFail Instr (GValueType x ': inp) out

instance GInstrCase x => GInstrCase (G.D1 i x) where
  type GCaseClauses (G.D1 i x) = GCaseClauses x
  gInstrCase :: Rec (CaseClause inp out) (GCaseClauses (D1 i x))
-> RemFail Instr (GValueType (D1 i x) : inp) out
gInstrCase = forall (inp :: [T]) (out :: [T]).
(GInstrCase x, GIsoValue x) =>
Rec (CaseClause inp out) (GCaseClauses x)
-> RemFail Instr (GValueType x : inp) out
forall (x :: * -> *) (inp :: [T]) (out :: [T]).
(GInstrCase x, GIsoValue x) =>
Rec (CaseClause inp out) (GCaseClauses x)
-> RemFail Instr (GValueType x : inp) out
gInstrCase @x

instance (GInstrCase x, GInstrCase y, RSplit (GCaseClauses x) (GCaseClauses y)) =>
         GInstrCase (x :+: y) where
  type GCaseClauses (x :+: y) = GCaseClauses x ++ GCaseClauses y
  gInstrCase :: Rec (CaseClause inp out) (GCaseClauses (x :+: y))
-> RemFail Instr (GValueType (x :+: y) : inp) out
gInstrCase clauses :: Rec (CaseClause inp out) (GCaseClauses (x :+: y))
clauses =
    let (leftClauses :: Rec (CaseClause inp out) (GCaseClauses x)
leftClauses, rightClauses :: Rec (CaseClause inp out) (GCaseClauses y)
rightClauses) = Rec (CaseClause inp out) (GCaseClauses x ++ GCaseClauses y)
-> (Rec (CaseClause inp out) (GCaseClauses x),
    Rec (CaseClause inp out) (GCaseClauses y))
forall k (l :: [k]) (r :: [k]) (f :: k -> *).
RSplit l r =>
Rec f (l ++ r) -> (Rec f l, Rec f r)
rsplit Rec (CaseClause inp out) (GCaseClauses x ++ GCaseClauses y)
Rec (CaseClause inp out) (GCaseClauses (x :+: y))
clauses
    in (forall (o' :: [T]).
 Instr (GValueType x : inp) o'
 -> Instr (GValueType y : inp) o'
 -> Instr ('TOr (GValueType x) (GValueType y) : inp) o')
-> RemFail Instr (GValueType x : inp) out
-> RemFail Instr (GValueType y : inp) out
-> RemFail Instr ('TOr (GValueType x) (GValueType y) : inp) out
forall k (instr :: k -> k -> *) (i1 :: k) (i2 :: k) (i3 :: k)
       (o :: k).
(forall (o' :: k). instr i1 o' -> instr i2 o' -> instr i3 o')
-> RemFail instr i1 o -> RemFail instr i2 o -> RemFail instr i3 o
rfMerge forall (o' :: [T]).
Instr (GValueType x : inp) o'
-> Instr (GValueType y : inp) o'
-> Instr ('TOr (GValueType x) (GValueType y) : inp) o'
forall (a :: T) (s :: [T]) (s' :: [T]) (b :: T).
Instr (a : s) s' -> Instr (b : s) s' -> Instr ('TOr a b : s) s'
IF_LEFT (Rec (CaseClause inp out) (GCaseClauses x)
-> RemFail Instr (GValueType x : inp) out
forall (x :: * -> *) (inp :: [T]) (out :: [T]).
(GInstrCase x, GIsoValue x) =>
Rec (CaseClause inp out) (GCaseClauses x)
-> RemFail Instr (GValueType x : inp) out
gInstrCase @x Rec (CaseClause inp out) (GCaseClauses x)
leftClauses) (Rec (CaseClause inp out) (GCaseClauses y)
-> RemFail Instr (GValueType y : inp) out
forall (x :: * -> *) (inp :: [T]) (out :: [T]).
(GInstrCase x, GIsoValue x) =>
Rec (CaseClause inp out) (GCaseClauses x)
-> RemFail Instr (GValueType x : inp) out
gInstrCase @y Rec (CaseClause inp out) (GCaseClauses y)
rightClauses)

instance GInstrCaseBranch ctor x => GInstrCase (G.C1 ('G.MetaCons ctor _1 _2) x) where
  type GCaseClauses (G.C1 ('G.MetaCons ctor _1 _2) x) = '[GCaseBranchInput ctor x]
  gInstrCase :: Rec
  (CaseClause inp out) (GCaseClauses (C1 ('MetaCons ctor _1 _2) x))
-> RemFail
     Instr (GValueType (C1 ('MetaCons ctor _1 _2) x) : inp) out
gInstrCase (clause :: CaseClause inp out r
clause :& RNil) = CaseClause inp out (GCaseBranchInput ctor x)
-> RemFail Instr (GValueType x : inp) out
forall (ctor :: Symbol) (x :: * -> *) (inp :: [T]) (out :: [T]).
GInstrCaseBranch ctor x =>
CaseClause inp out (GCaseBranchInput ctor x)
-> RemFail Instr (GValueType x : inp) out
gInstrCaseBranch @ctor @x CaseClause inp out r
CaseClause inp out (GCaseBranchInput ctor x)
clause

-- | Traverse a single contructor and supply its field to instruction in case clause.
class GIsoValue x =>
      GInstrCaseBranch (ctor :: Symbol) (x :: Kind.Type -> Kind.Type) where

  type GCaseBranchInput ctor x :: CaseClauseParam

  gInstrCaseBranch
    :: CaseClause inp out (GCaseBranchInput ctor x)
    -> RemFail Instr (GValueType x ': inp) out

instance
  ( GIsoValue x, GIsoValue y
  , TypeError ('Text "Cannot pattern match on constructors with more than 1 field"
               ':$$: 'Text "Consider using tuples instead")
  ) => GInstrCaseBranch ctor (x :*: y) where

  type GCaseBranchInput ctor (x :*: y) = 'CaseClauseParam ctor 'NoFields
  gInstrCaseBranch :: CaseClause inp out (GCaseBranchInput ctor (x :*: y))
-> RemFail Instr (GValueType (x :*: y) : inp) out
gInstrCaseBranch = Text
-> CaseClause inp out ('CaseClauseParam ctor 'NoFields)
-> RemFail Instr ('TPair (GValueType x) (GValueType y) : inp) out
forall a. HasCallStack => Text -> a
error "impossible"

instance GInstrCaseBranch ctor x => GInstrCaseBranch ctor (G.S1 i x) where
  type GCaseBranchInput ctor (G.S1 i x) = GCaseBranchInput ctor x
  gInstrCaseBranch :: CaseClause inp out (GCaseBranchInput ctor (S1 i x))
-> RemFail Instr (GValueType (S1 i x) : inp) out
gInstrCaseBranch = forall (inp :: [T]) (out :: [T]).
GInstrCaseBranch ctor x =>
CaseClause inp out (GCaseBranchInput ctor x)
-> RemFail Instr (GValueType x : inp) out
forall (ctor :: Symbol) (x :: * -> *) (inp :: [T]) (out :: [T]).
GInstrCaseBranch ctor x =>
CaseClause inp out (GCaseBranchInput ctor x)
-> RemFail Instr (GValueType x : inp) out
gInstrCaseBranch @ctor @x

instance IsoValue a => GInstrCaseBranch ctor (G.Rec0 a) where
  type GCaseBranchInput ctor (G.Rec0 a) = 'CaseClauseParam ctor ('OneField a)
  gInstrCaseBranch :: CaseClause inp out (GCaseBranchInput ctor (Rec0 a))
-> RemFail Instr (GValueType (Rec0 a) : inp) out
gInstrCaseBranch (CaseClause i :: RemFail Instr (AppendCtorField x inp) out
i) = RemFail Instr (GValueType (Rec0 a) : inp) out
RemFail Instr (AppendCtorField x inp) out
i

instance GInstrCaseBranch ctor G.U1 where
  type GCaseBranchInput ctor G.U1 = 'CaseClauseParam ctor 'NoFields
  gInstrCaseBranch :: CaseClause inp out (GCaseBranchInput ctor U1)
-> RemFail Instr (GValueType U1 : inp) out
gInstrCaseBranch (CaseClause i :: RemFail Instr (AppendCtorField x inp) out
i) = (forall (o' :: [T]). Instr inp o' -> Instr ('TUnit : inp) o')
-> RemFail Instr inp out -> RemFail Instr ('TUnit : inp) out
forall k (instr :: k -> k -> *) (i1 :: k) (i2 :: k) (o :: k).
(forall (o' :: k). instr i1 o' -> instr i2 o')
-> RemFail instr i1 o -> RemFail instr i2 o
rfMapAnyInstr (Instr ('TUnit : inp) inp
forall (a :: T) (s :: [T]). Instr (a : s) s
DROP Instr ('TUnit : inp) inp -> Instr inp o' -> Instr ('TUnit : inp) o'
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq`) RemFail Instr inp out
RemFail Instr (AppendCtorField x inp) out
i

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

_caseMyType :: RemFail Instr (ToT MyType ': s) (ToT Integer ': s)
_caseMyType :: RemFail Instr (ToT MyType : s) (ToT Integer : s)
_caseMyType = forall (out :: [T]) (inp :: [T]).
InstrCaseC MyType =>
Rec (CaseClause inp out) (CaseClauses MyType)
-> RemFail Instr (ToT MyType : inp) out
forall dt (out :: [T]) (inp :: [T]).
InstrCaseC dt =>
Rec (CaseClause inp out) (CaseClauses dt)
-> RemFail Instr (ToT dt : inp) out
instrCase @MyType (Rec (CaseClause s ('TInt : s)) (CaseClauses MyType)
 -> RemFail Instr (ToT MyType : s) (ToT Integer : s))
-> Rec (CaseClause s ('TInt : s)) (CaseClauses MyType)
-> RemFail Instr (ToT MyType : s) (ToT Integer : s)
forall a b. (a -> b) -> a -> b
$
     #cMyCtor //-> RfNormal Nop
  :& #cComplexThing //-> RfNormal (DROP `Seq` PUSH (toVal @Integer 5))
  :& #cUselessThing //-> RfNormal (DROP `Seq` PUSH (toVal @Integer 0))
  :& RNil

-- Another version, written via tuple.
_caseMyType2 :: RemFail Instr (ToT MyType ': s) (ToT Integer ': s)
_caseMyType2 :: RemFail Instr (ToT MyType : s) (ToT Integer : s)
_caseMyType2 = forall (out :: [T]) (inp :: [T]).
InstrCaseC MyType =>
Rec (CaseClause inp out) (CaseClauses MyType)
-> RemFail Instr (ToT MyType : inp) out
forall dt (out :: [T]) (inp :: [T]).
InstrCaseC dt =>
Rec (CaseClause inp out) (CaseClauses dt)
-> RemFail Instr (ToT dt : inp) out
instrCase @MyType (Rec (CaseClause s ('TInt : s)) (CaseClauses MyType)
 -> RemFail Instr (ToT MyType : s) (ToT Integer : s))
-> Rec (CaseClause s ('TInt : s)) (CaseClauses MyType)
-> RemFail Instr (ToT MyType : s) (ToT Integer : s)
forall a b. (a -> b) -> a -> b
$ IsoRecTuple
  (Rec
     (CaseClause s ('TInt : s))
     '[ 'CaseClauseParam "MyCtor" ('OneField Integer),
        'CaseClauseParam "ComplexThing" ('OneField ()),
        'CaseClauseParam
          "UselessThing"
          ('OneField ("field1" :! ByteString, "field2" :! ()))])
-> Rec
     (CaseClause s ('TInt : s))
     '[ 'CaseClauseParam "MyCtor" ('OneField Integer),
        'CaseClauseParam "ComplexThing" ('OneField ()),
        'CaseClauseParam
          "UselessThing"
          ('OneField ("field1" :! ByteString, "field2" :! ()))]
forall r. RecFromTuple r => IsoRecTuple r -> r
recFromTuple
  ( IsLabel "cMyCtor" (Label "cMyCtor")
Label (AppendSymbol "c" "MyCtor")
#cMyCtor Label (AppendSymbol "c" "MyCtor")
-> RemFail
     Instr (AppendCtorField ('OneField Integer) s) ('TInt : s)
-> CaseClause
     s ('TInt : s) ('CaseClauseParam "MyCtor" ('OneField Integer))
forall (ctor :: Symbol) (x :: CtorField) (inp :: [T]) (out :: [T]).
Label (AppendSymbol "c" ctor)
-> RemFail Instr (AppendCtorField x inp) out
-> CaseClause inp out ('CaseClauseParam ctor x)
//->
      Instr ('TInt : s) ('TInt : s)
-> RemFail Instr ('TInt : s) ('TInt : s)
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr ('TInt : s) ('TInt : s)
forall (s :: [T]). Instr s s
Nop
  , IsLabel "cComplexThing" (Label "cComplexThing")
Label (AppendSymbol "c" "ComplexThing")
#cComplexThing Label (AppendSymbol "c" "ComplexThing")
-> RemFail Instr (AppendCtorField ('OneField ()) s) ('TInt : s)
-> CaseClause
     s ('TInt : s) ('CaseClauseParam "ComplexThing" ('OneField ()))
forall (ctor :: Symbol) (x :: CtorField) (inp :: [T]) (out :: [T]).
Label (AppendSymbol "c" ctor)
-> RemFail Instr (AppendCtorField x inp) out
-> CaseClause inp out ('CaseClauseParam ctor x)
//->
      Instr ('TUnit : s) ('TInt : s)
-> RemFail Instr ('TUnit : s) ('TInt : s)
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (Instr ('TUnit : s) s
forall (a :: T) (s :: [T]). Instr (a : s) s
DROP Instr ('TUnit : s) s
-> Instr s ('TInt : s) -> Instr ('TUnit : s) ('TInt : s)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` 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))
  , IsLabel "cUselessThing" (Label "cUselessThing")
Label (AppendSymbol "c" "UselessThing")
#cUselessThing Label (AppendSymbol "c" "UselessThing")
-> RemFail
     Instr
     (AppendCtorField
        ('OneField ("field1" :! ByteString, "field2" :! ())) s)
     ('TInt : s)
-> CaseClause
     s
     ('TInt : s)
     ('CaseClauseParam
        "UselessThing"
        ('OneField ("field1" :! ByteString, "field2" :! ())))
forall (ctor :: Symbol) (x :: CtorField) (inp :: [T]) (out :: [T]).
Label (AppendSymbol "c" ctor)
-> RemFail Instr (AppendCtorField x inp) out
-> CaseClause inp out ('CaseClauseParam ctor x)
//->
      Instr ('TPair 'TBytes 'TUnit : s) ('TInt : s)
-> RemFail Instr ('TPair 'TBytes 'TUnit : s) ('TInt : s)
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (Instr ('TPair 'TBytes 'TUnit : s) s
forall (a :: T) (s :: [T]). Instr (a : s) s
DROP Instr ('TPair 'TBytes 'TUnit : s) s
-> Instr s ('TInt : s)
-> Instr ('TPair 'TBytes 'TUnit : s) ('TInt : s)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` 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 0))
  )

_caseMyEnum :: RemFail Instr (ToT MyEnum ': ToT Integer ': s) (ToT Integer ': s)
_caseMyEnum :: RemFail Instr (ToT MyEnum : ToT Integer : s) (ToT Integer : s)
_caseMyEnum = forall (out :: [T]) (inp :: [T]).
InstrCaseC MyEnum =>
Rec (CaseClause inp out) (CaseClauses MyEnum)
-> RemFail Instr (ToT MyEnum : inp) out
forall dt (out :: [T]) (inp :: [T]).
InstrCaseC dt =>
Rec (CaseClause inp out) (CaseClauses dt)
-> RemFail Instr (ToT dt : inp) out
instrCase @MyEnum (Rec (CaseClause ('TInt : s) ('TInt : s)) (CaseClauses MyEnum)
 -> RemFail Instr (ToT MyEnum : ToT Integer : s) (ToT Integer : s))
-> Rec (CaseClause ('TInt : s) ('TInt : s)) (CaseClauses MyEnum)
-> RemFail Instr (ToT MyEnum : ToT Integer : s) (ToT Integer : s)
forall a b. (a -> b) -> a -> b
$ IsoRecTuple
  (Rec
     (CaseClause ('TInt : s) ('TInt : s))
     '[ 'CaseClauseParam "Case1" 'NoFields,
        'CaseClauseParam "Case2" 'NoFields,
        'CaseClauseParam "CaseN" ('OneField Integer),
        'CaseClauseParam "CaseDef" 'NoFields])
-> Rec
     (CaseClause ('TInt : s) ('TInt : s))
     '[ 'CaseClauseParam "Case1" 'NoFields,
        'CaseClauseParam "Case2" 'NoFields,
        'CaseClauseParam "CaseN" ('OneField Integer),
        'CaseClauseParam "CaseDef" 'NoFields]
forall r. RecFromTuple r => IsoRecTuple r -> r
recFromTuple
  ( IsLabel "cCase1" (Label "cCase1")
Label (AppendSymbol "c" "Case1")
#cCase1 Label (AppendSymbol "c" "Case1")
-> RemFail
     Instr (AppendCtorField 'NoFields ('TInt : s)) ('TInt : s)
-> CaseClause
     ('TInt : s) ('TInt : s) ('CaseClauseParam "Case1" 'NoFields)
forall (ctor :: Symbol) (x :: CtorField) (inp :: [T]) (out :: [T]).
Label (AppendSymbol "c" ctor)
-> RemFail Instr (AppendCtorField x inp) out
-> CaseClause inp out ('CaseClauseParam ctor x)
//-> Instr ('TInt : s) ('TInt : s)
-> RemFail Instr ('TInt : s) ('TInt : s)
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (Instr ('TInt : s) s
forall (a :: T) (s :: [T]). Instr (a : s) s
DROP Instr ('TInt : s) s
-> Instr s ('TInt : s) -> Instr ('TInt : s) ('TInt : s)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` 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 1))
  , IsLabel "cCase2" (Label "cCase2")
Label (AppendSymbol "c" "Case2")
#cCase2 Label (AppendSymbol "c" "Case2")
-> RemFail
     Instr (AppendCtorField 'NoFields ('TInt : s)) ('TInt : s)
-> CaseClause
     ('TInt : s) ('TInt : s) ('CaseClauseParam "Case2" 'NoFields)
forall (ctor :: Symbol) (x :: CtorField) (inp :: [T]) (out :: [T]).
Label (AppendSymbol "c" ctor)
-> RemFail Instr (AppendCtorField x inp) out
-> CaseClause inp out ('CaseClauseParam ctor x)
//-> Instr ('TInt : s) ('TInt : s)
-> RemFail Instr ('TInt : s) ('TInt : s)
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (Instr ('TInt : s) s
forall (a :: T) (s :: [T]). Instr (a : s) s
DROP Instr ('TInt : s) s
-> Instr s ('TInt : s) -> Instr ('TInt : s) ('TInt : s)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` 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 2))
  , IsLabel "cCaseN" (Label "cCaseN")
Label (AppendSymbol "c" "CaseN")
#cCaseN Label (AppendSymbol "c" "CaseN")
-> RemFail
     Instr (AppendCtorField ('OneField Integer) ('TInt : s)) ('TInt : s)
-> CaseClause
     ('TInt : s)
     ('TInt : s)
     ('CaseClauseParam "CaseN" ('OneField Integer))
forall (ctor :: Symbol) (x :: CtorField) (inp :: [T]) (out :: [T]).
Label (AppendSymbol "c" ctor)
-> RemFail Instr (AppendCtorField x inp) out
-> CaseClause inp out ('CaseClauseParam ctor x)
//-> Instr ('TInt : 'TInt : s) ('TInt : s)
-> RemFail Instr ('TInt : 'TInt : s) ('TInt : s)
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (Instr ('TInt : s) s -> Instr ('TInt : 'TInt : s) ('TInt : s)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr ('TInt : s) s
forall (a :: T) (s :: [T]). Instr (a : s) s
DROP Instr ('TInt : 'TInt : s) ('TInt : s)
-> Instr ('TInt : s) ('TInt : s)
-> Instr ('TInt : 'TInt : s) ('TInt : s)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr ('TInt : s) ('TInt : s)
forall (s :: [T]). Instr s s
Nop)
  , IsLabel "cCaseDef" (Label "cCaseDef")
Label (AppendSymbol "c" "CaseDef")
#cCaseDef Label (AppendSymbol "c" "CaseDef")
-> RemFail
     Instr (AppendCtorField 'NoFields ('TInt : s)) ('TInt : s)
-> CaseClause
     ('TInt : s) ('TInt : s) ('CaseClauseParam "CaseDef" 'NoFields)
forall (ctor :: Symbol) (x :: CtorField) (inp :: [T]) (out :: [T]).
Label (AppendSymbol "c" ctor)
-> RemFail Instr (AppendCtorField x inp) out
-> CaseClause inp out ('CaseClauseParam ctor x)
//-> Instr ('TInt : s) ('TInt : s)
-> RemFail Instr ('TInt : s) ('TInt : s)
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr ('TInt : s) ('TInt : s)
forall (s :: [T]). Instr s s
Nop
  )

----------------------------------------------------------------------------
-- Constructor unwrapping instruction
----------------------------------------------------------------------------

-- | Unwrap a constructor with the given name.
--
-- Rules which apply to 'instrWrap' function work here as well.
-- Although, unlike @instrWrap@, this function does not work for nullary
-- constructors.
instrUnwrapUnsafe
  :: forall dt name st.
     InstrUnwrapC dt name
  => Label name
  -> Instr (ToT dt ': st)
           (ToT (CtorOnlyField name dt) ': st)
instrUnwrapUnsafe :: Label name
-> Instr (ToT dt : st) (ToT (CtorOnlyField name dt) : st)
instrUnwrapUnsafe _ =
  forall (s :: [T]).
(GInstrUnwrap
   (Rep dt) (LnrBranch (GetNamed name dt)) (CtorOnlyField name dt),
 GIsoValue (Rep dt)) =>
Instr (GValueType (Rep dt) : s) (ToT (CtorOnlyField name dt) : s)
forall (x :: * -> *) (path :: Path) entryTy (s :: [T]).
(GInstrUnwrap x path entryTy, GIsoValue x) =>
Instr (GValueType x : s) (ToT entryTy : s)
gInstrUnwrapUnsafe @(G.Rep dt) @(LnrBranch (GetNamed name dt))
                                 @(CtorOnlyField name dt)

type InstrUnwrapC dt name =
  ( GenericIsoValue dt
  , GInstrUnwrap (G.Rep dt)
      (LnrBranch (GetNamed name dt))
      (CtorOnlyField name dt)
  )

-- | Try to unwrap a constructor with the given name.
hsUnwrap
  :: forall dt name.
     InstrUnwrapC dt name
  => Label name
  -> dt
  -> Maybe (CtorOnlyField name dt)
hsUnwrap :: Label name -> dt -> Maybe (CtorOnlyField name dt)
hsUnwrap _ =
  forall p.
GInstrUnwrap
  (Rep dt) (LnrBranch (GetNamed name dt)) (CtorOnlyField name dt) =>
Rep dt p -> Maybe (CtorOnlyField name dt)
forall (x :: * -> *) (path :: Path) entryTy p.
GInstrUnwrap x path entryTy =>
x p -> Maybe entryTy
gHsUnwrap @(G.Rep dt) @(LnrBranch (GetNamed name dt))
            @(CtorOnlyField name dt) (Rep dt Any -> Maybe (CtorOnlyField name dt))
-> (dt -> Rep dt Any) -> dt -> Maybe (CtorOnlyField name dt)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  dt -> Rep dt Any
forall a x. Generic a => a -> Rep a x
G.from

class GIsoValue x =>
  GInstrUnwrap
    (x :: Kind.Type -> Kind.Type)
    (path :: Path)
    (entryTy :: Kind.Type) where
  gInstrUnwrapUnsafe
    :: GIsoValue x
    => Instr (GValueType x ': s) (ToT entryTy ': s)
  gHsUnwrap
    :: x p -> Maybe entryTy

instance GInstrUnwrap x path e => GInstrUnwrap (G.D1 i x) path e where
  gInstrUnwrapUnsafe :: Instr (GValueType (D1 i x) : s) (ToT e : s)
gInstrUnwrapUnsafe = forall (s :: [T]).
(GInstrUnwrap x path e, GIsoValue x) =>
Instr (GValueType x : s) (ToT e : s)
forall (x :: * -> *) (path :: Path) entryTy (s :: [T]).
(GInstrUnwrap x path entryTy, GIsoValue x) =>
Instr (GValueType x : s) (ToT entryTy : s)
gInstrUnwrapUnsafe @x @path @e
  gHsUnwrap :: D1 i x p -> Maybe e
gHsUnwrap = forall p. GInstrUnwrap x path e => x p -> Maybe e
forall (x :: * -> *) (path :: Path) entryTy p.
GInstrUnwrap x path entryTy =>
x p -> Maybe entryTy
gHsUnwrap @x @path @e (x p -> Maybe e) -> (D1 i x p -> x p) -> D1 i x p -> Maybe e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. D1 i x p -> x p
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1

instance (GInstrUnwrap x path e, GIsoValue y, SingI (GValueType y)) =>
         GInstrUnwrap (x :+: y) ('L ': path) e where
  gInstrUnwrapUnsafe :: Instr (GValueType (x :+: y) : s) (ToT e : s)
gInstrUnwrapUnsafe = Instr (GValueType x : s) (ToT e : s)
-> Instr (GValueType y : s) (ToT e : s)
-> Instr ('TOr (GValueType x) (GValueType y) : s) (ToT e : s)
forall (a :: T) (s :: [T]) (s' :: [T]) (b :: T).
Instr (a : s) s' -> Instr (b : s) s' -> Instr ('TOr a b : s) s'
IF_LEFT (forall (s :: [T]).
(GInstrUnwrap x path e, GIsoValue x) =>
Instr (GValueType x : s) (ToT e : s)
forall (x :: * -> *) (path :: Path) entryTy (s :: [T]).
(GInstrUnwrap x path entryTy, GIsoValue x) =>
Instr (GValueType x : s) (ToT entryTy : s)
gInstrUnwrapUnsafe @x @path @e) Instr (GValueType y : s) (ToT e : s)
forall (i :: [T]) (o :: [T]). Instr i o
failWithWrongCtor
  gHsUnwrap :: (:+:) x y p -> Maybe e
gHsUnwrap = \case
    G.L1 x :: x p
x -> x p -> Maybe e
forall (x :: * -> *) (path :: Path) entryTy p.
GInstrUnwrap x path entryTy =>
x p -> Maybe entryTy
gHsUnwrap @x @path @e x p
x
    G.R1 _ -> Maybe e
forall a. Maybe a
Nothing

instance (GInstrUnwrap y path e, GIsoValue x, SingI (GValueType x)) =>
         GInstrUnwrap (x :+: y) ('R ': path) e where
  gInstrUnwrapUnsafe :: Instr (GValueType (x :+: y) : s) (ToT e : s)
gInstrUnwrapUnsafe = Instr (GValueType x : s) (ToT e : s)
-> Instr (GValueType y : s) (ToT e : s)
-> Instr ('TOr (GValueType x) (GValueType y) : s) (ToT e : s)
forall (a :: T) (s :: [T]) (s' :: [T]) (b :: T).
Instr (a : s) s' -> Instr (b : s) s' -> Instr ('TOr a b : s) s'
IF_LEFT Instr (GValueType x : s) (ToT e : s)
forall (i :: [T]) (o :: [T]). Instr i o
failWithWrongCtor (forall (s :: [T]).
(GInstrUnwrap y path e, GIsoValue y) =>
Instr (GValueType y : s) (ToT e : s)
forall (x :: * -> *) (path :: Path) entryTy (s :: [T]).
(GInstrUnwrap x path entryTy, GIsoValue x) =>
Instr (GValueType x : s) (ToT entryTy : s)
gInstrUnwrapUnsafe @y @path @e)
  gHsUnwrap :: (:+:) x y p -> Maybe e
gHsUnwrap = \case
    G.R1 y :: y p
y -> y p -> Maybe e
forall (x :: * -> *) (path :: Path) entryTy p.
GInstrUnwrap x path entryTy =>
x p -> Maybe entryTy
gHsUnwrap @y @path @e y p
y
    G.L1 _ -> Maybe e
forall a. Maybe a
Nothing

instance (IsoValue e) =>
         GInstrUnwrap (G.C1 c (G.S1 i (G.Rec0 e))) '[ 'S] e where
  gInstrUnwrapUnsafe :: Instr (GValueType (C1 c (S1 i (Rec0 e))) : s) (ToT e : s)
gInstrUnwrapUnsafe = Instr (GValueType (C1 c (S1 i (Rec0 e))) : s) (ToT e : s)
forall (s :: [T]). Instr s s
Nop
  gHsUnwrap :: C1 c (S1 i (Rec0 e)) p -> Maybe e
gHsUnwrap = e -> Maybe e
forall a. a -> Maybe a
Just (e -> Maybe e)
-> (C1 c (S1 i (Rec0 e)) p -> e)
-> C1 c (S1 i (Rec0 e)) p
-> Maybe e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 R e p -> e
forall i c k (p :: k). K1 i c p -> c
G.unK1 (K1 R e p -> e)
-> (C1 c (S1 i (Rec0 e)) p -> K1 R e p)
-> C1 c (S1 i (Rec0 e)) p
-> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 S i (Rec0 e) p -> K1 R e p
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1 (M1 S i (Rec0 e) p -> K1 R e p)
-> (C1 c (S1 i (Rec0 e)) p -> M1 S i (Rec0 e) p)
-> C1 c (S1 i (Rec0 e)) p
-> K1 R e p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. C1 c (S1 i (Rec0 e)) p -> M1 S i (Rec0 e) p
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1

-- This is the case when a sum type is part of another sum type.
-- Here 'sub' is intermediate sum type.
instance ( path ~ (x ': xs)
         , GInstrUnwrap (G.Rep sub) path e
         , GenericIsoValue sub
         , GIsoValue (G.Rep sub)
         ) =>
         GInstrUnwrap (G.C1 c (G.S1 i (G.Rec0 sub))) ('S ': x ': xs) e where
  gInstrUnwrapUnsafe :: Instr (GValueType (C1 c (S1 i (Rec0 sub))) : s) (ToT e : s)
gInstrUnwrapUnsafe = forall (s :: [T]).
(GInstrUnwrap (Rep sub) path e, GIsoValue (Rep sub)) =>
Instr (GValueType (Rep sub) : s) (ToT e : s)
forall (x :: * -> *) (path :: Path) entryTy (s :: [T]).
(GInstrUnwrap x path entryTy, GIsoValue x) =>
Instr (GValueType x : s) (ToT entryTy : s)
gInstrUnwrapUnsafe @(G.Rep sub) @path @e
  gHsUnwrap :: C1 c (S1 i (Rec0 sub)) p -> Maybe e
gHsUnwrap = forall p. GInstrUnwrap (Rep sub) path e => Rep sub p -> Maybe e
forall (x :: * -> *) (path :: Path) entryTy p.
GInstrUnwrap x path entryTy =>
x p -> Maybe entryTy
gHsUnwrap @(G.Rep sub) @path @e (Rep sub Any -> Maybe e)
-> (C1 c (S1 i (Rec0 sub)) p -> Rep sub Any)
-> C1 c (S1 i (Rec0 sub)) p
-> Maybe e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sub -> Rep sub Any
forall a x. Generic a => a -> Rep a x
G.from (sub -> Rep sub Any)
-> (C1 c (S1 i (Rec0 sub)) p -> sub)
-> C1 c (S1 i (Rec0 sub)) p
-> Rep sub Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 R sub p -> sub
forall i c k (p :: k). K1 i c p -> c
G.unK1 (K1 R sub p -> sub)
-> (C1 c (S1 i (Rec0 sub)) p -> K1 R sub p)
-> C1 c (S1 i (Rec0 sub)) p
-> sub
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 S i (Rec0 sub) p -> K1 R sub p
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1 (M1 S i (Rec0 sub) p -> K1 R sub p)
-> (C1 c (S1 i (Rec0 sub)) p -> M1 S i (Rec0 sub) p)
-> C1 c (S1 i (Rec0 sub)) p
-> K1 R sub p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. C1 c (S1 i (Rec0 sub)) p -> M1 S i (Rec0 sub) p
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1

-- | Failure indicating that we expected value created with one constructor,
-- but got value with different one.
-- The error message is intentionally ugly to keep it relatively short and
-- save on gas.
failWithWrongCtor :: Instr i o
failWithWrongCtor :: Instr i o
failWithWrongCtor =
  Value' Instr 'TString -> Instr i ('TString : i)
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 [mt|BadCtor|]) Instr i ('TString : i) -> Instr ('TString : i) o -> Instr i o
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq`
  Instr ('TString : i) o
forall (a :: T) (s :: [T]) (t :: [T]). KnownT a => Instr (a : s) t
FAILWITH

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

_unwrapMyType :: Instr (ToT MyType ': s) (ToT Integer ': s)
_unwrapMyType :: Instr (ToT MyType : s) (ToT Integer : s)
_unwrapMyType = Label "cMyCtor"
-> Instr
     (ToT MyType : s) (ToT (CtorOnlyField "cMyCtor" MyType) : s)
forall dt (name :: Symbol) (st :: [T]).
InstrUnwrapC dt name =>
Label name
-> Instr (ToT dt : st) (ToT (CtorOnlyField name dt) : st)
instrUnwrapUnsafe @MyType IsLabel "cMyCtor" (Label "cMyCtor")
Label "cMyCtor"
#cMyCtor

_unwrapMyCompoundType :: Instr (ToT MyCompoundType ': s) (ToT Integer ': s)
_unwrapMyCompoundType :: Instr (ToT MyCompoundType : s) (ToT Integer : s)
_unwrapMyCompoundType = Label "cMyCtor"
-> Instr
     (ToT MyCompoundType : s)
     (ToT (CtorOnlyField "cMyCtor" MyCompoundType) : s)
forall dt (name :: Symbol) (st :: [T]).
InstrUnwrapC dt name =>
Label name
-> Instr (ToT dt : st) (ToT (CtorOnlyField name dt) : st)
instrUnwrapUnsafe @MyCompoundType IsLabel "cMyCtor" (Label "cMyCtor")
Label "cMyCtor"
#cMyCtor

_unwrapMyCompoundType2 :: Instr (ToT MyCompoundType ': s) (ToT Address ': s)
_unwrapMyCompoundType2 :: Instr (ToT MyCompoundType : s) (ToT Address : s)
_unwrapMyCompoundType2 = Label "cCompoundPart3"
-> Instr
     (ToT MyCompoundType : s)
     (ToT (CtorOnlyField "cCompoundPart3" MyCompoundType) : s)
forall dt (name :: Symbol) (st :: [T]).
InstrUnwrapC dt name =>
Label name
-> Instr (ToT dt : st) (ToT (CtorOnlyField name dt) : st)
instrUnwrapUnsafe @MyCompoundType IsLabel "cCompoundPart3" (Label "cCompoundPart3")
Label "cCompoundPart3"
#cCompoundPart3

_unwrapMyCompoundType3 :: Instr (ToT MyCompoundType ': s) (ToT Bool ': s)
_unwrapMyCompoundType3 :: Instr (ToT MyCompoundType : s) (ToT Bool : s)
_unwrapMyCompoundType3 = Label "cWrapBool"
-> Instr
     (ToT MyCompoundType : s)
     (ToT (CtorOnlyField "cWrapBool" MyCompoundType) : s)
forall dt (name :: Symbol) (st :: [T]).
InstrUnwrapC dt name =>
Label name
-> Instr (ToT dt : st) (ToT (CtorOnlyField name dt) : st)
instrUnwrapUnsafe @MyCompoundType IsLabel "cWrapBool" (Label "cWrapBool")
Label "cWrapBool"
#cWrapBool

_unwrapMyCompoundType4 :: Instr (ToT MyCompoundType ': s) (ToT MyType' ': s)
_unwrapMyCompoundType4 :: Instr (ToT MyCompoundType : s) (ToT MyType' : s)
_unwrapMyCompoundType4 = Label "cCompoundPart4"
-> Instr
     (ToT MyCompoundType : s)
     (ToT (CtorOnlyField "cCompoundPart4" MyCompoundType) : s)
forall dt (name :: Symbol) (st :: [T]).
InstrUnwrapC dt name =>
Label name
-> Instr (ToT dt : st) (ToT (CtorOnlyField name dt) : st)
instrUnwrapUnsafe @MyCompoundType IsLabel "cCompoundPart4" (Label "cCompoundPart4")
Label "cCompoundPart4"
#cCompoundPart4