{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Morley.Michelson.Typed.Haskell.Instr.Sum
( InstrWrapC
, InstrWrapOneC
, InstrCaseC
, InstrUnwrapC
, instrWrap
, instrWrapOne
, hsWrap
, instrCase
, (//->)
, unsafeInstrUnwrap
, hsUnwrap
, CaseClauseParam (..)
, CaseClause (..)
, CaseClauses
, GCaseClauses
, GCaseBranchInput
, Branch (..)
, Path
, CtorField (..)
, ExtractCtorField
, AppendCtorField
, AppendCtorFieldAxiom
, appendCtorFieldAxiom
, GetCtorField
, CtorHasOnlyField
, CtorOnlyField
, MyCompoundType
, IsPrimitiveValue
) where
import Data.Constraint (Bottom(..))
import Data.Singletons (SingI(..))
import Data.Type.Bool (type (||))
import Data.Vinyl.Core (Rec(..))
import GHC.Generics ((:*:)(..), (:+:)(..))
import GHC.Generics qualified as G
import GHC.TypeLits (AppendSymbol, ErrorMessage(..), Symbol, TypeError)
import Type.Reflection ((:~:)(Refl))
import Unsafe.Coerce (unsafeCoerce)
import Morley.Michelson.Text (MText, mt)
import Morley.Michelson.Typed.Entrypoints
import Morley.Michelson.Typed.Haskell.Instr.Helpers
import Morley.Michelson.Typed.Haskell.Value
import Morley.Michelson.Typed.Instr
import Morley.Michelson.Typed.T
import Morley.Michelson.Typed.Value
import Morley.Tezos.Address (Address)
import Morley.Tezos.Core (ChainId, Mutez, Timestamp)
import Morley.Tezos.Crypto (KeyHash, PublicKey, Signature)
import Morley.Util.Generic
import Morley.Util.Label (Label)
import Morley.Util.Named
import Morley.Util.Type
import Morley.Util.TypeTuple
data CtorField
= OneField Type
| NoFields
type family (cf :: CtorField) where
('OneField t) = t
'NoFields = ()
type AppendCtorField :: CtorField -> [k] -> [k]
type family AppendCtorField cf l where
AppendCtorField ('OneField t) (l :: [T]) = ToT t ': l
AppendCtorField ('OneField t) (l :: [Type]) = t ': l
AppendCtorField 'NoFields (l :: [T]) = l
AppendCtorField 'NoFields (l :: [Type]) = l
type AppendCtorFieldAxiom (cf :: CtorField) (st :: [Type]) =
ToTs (AppendCtorField cf st) ~ AppendCtorField cf (ToTs st)
appendCtorFieldAxiom
:: ( AppendCtorFieldAxiom ('OneField Word) '[Int]
, AppendCtorFieldAxiom 'NoFields '[Int]
)
=> Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom :: forall (cf :: CtorField) (st :: [*]).
(AppendCtorFieldAxiom ('OneField Word) '[Int],
AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom =
Dict (AppendCtorFieldAxiom 'NoFields '[])
-> Dict (AppendCtorFieldAxiom cf st)
forall a b. a -> b
unsafeCoerce (Dict (AppendCtorFieldAxiom 'NoFields '[])
-> Dict (AppendCtorFieldAxiom cf st))
-> Dict (AppendCtorFieldAxiom 'NoFields '[])
-> Dict (AppendCtorFieldAxiom cf st)
forall a b. (a -> b) -> a -> b
$ forall (a :: Constraint). a => Dict a
Dict @(AppendCtorFieldAxiom 'NoFields '[])
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
type GetNamed name a = LNRequireFound name a (GLookupNamed name (GRep a))
type family LNRequireFound
(name :: Symbol)
(a :: Type)
(mf :: Maybe LookupNamedResult)
:: LookupNamedResult where
LNRequireFound _ _ ('Just lnr) = lnr
LNRequireFound name a 'Nothing = TypeError
('Text "Datatype " ':<>: 'ShowType a ':<>:
'Text " has no (sub)constructor " ':<>: 'ShowType name)
type family GLookupNamed (name :: Symbol) (x :: Type -> Type)
:: Maybe LookupNamedResult where
GLookupNamed name (G.D1 _ x) = GLookupNamed name x
GLookupNamed name (G.C1 ('G.MetaCons ctorName _ _) x) =
PrependS
(If (name == ctorName || name == ("c" `AppendSymbol` ctorName))
('Just $ 'LNR (GExtractFields x) '[])
(If (GCanGoDeeper x)
(GLookupNamedDeeper name x)
'Nothing
)
)
GLookupNamed name (x :+: y) =
LNMergeFound name (GLookupNamed name x) (GLookupNamed name y)
GLookupNamed _ G.V1 = 'Nothing
type family PrependS (x :: Maybe LookupNamedResult) :: Maybe LookupNamedResult where
PrependS 'Nothing = 'Nothing
PrependS ('Just ('LNR cf path)) = 'Just ('LNR cf ('S ': path))
type family GCanGoDeeper (x :: Type -> 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)
type family IsPrimitiveValue (x :: 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
type CanGoDeeper (x :: Type) =
If (IsPrimitiveValue x)
'False
(GCanGoDeeper (GRep x))
type family GLookupNamedDeeper (name :: Symbol) (x :: Type -> Type)
:: Maybe LookupNamedResult where
GLookupNamedDeeper name (G.S1 _ (G.Rec0 y)) = GLookupNamed name (GRep 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 (x :: Type -> Type)
:: CtorField where
(G.S1 _ x) = GExtractFields x
(G.Rec0 a) = 'OneField a
G.U1 = 'NoFields
(_ :*: _) = TypeError
('Text "Cannot automatically lookup constructors having multiple fields"
':$$:
'Text "Consider using tuple instead")
type GetCtorField dt ctor =
LnrFieldType (GetNamed ctor dt)
type CtorHasOnlyField ctor dt f =
GetCtorField dt ctor ~ 'OneField f
type family RequireOneField (ctor :: Symbol) (cf :: CtorField) :: Type where
RequireOneField _ ('OneField f) = f
RequireOneField ctor 'NoFields = TypeError
('Text "Expected exactly one field" ':$$:
'Text "In constructor " ':<>: 'ShowType ctor)
type CtorOnlyField name dt =
RequireOneField name (GetCtorField dt name)
instrWrap
:: forall dt name st.
InstrWrapC dt name
=> Label name
-> Instr (AppendCtorField (GetCtorField dt name) st)
(ToT dt ': st)
instrWrap :: forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap Label name
_ =
forall (x :: * -> *) (path :: Path) (entryTy :: CtorField)
(s :: [T]).
GInstrWrap x path entryTy =>
Instr (AppendCtorField entryTy s) (GValueType x : s)
gInstrWrap @(GRep dt) @(LnrBranch (GetNamed name dt))
@(LnrFieldType (GetNamed name dt))
instrWrapOne
:: forall dt name st.
InstrWrapOneC dt name
=> Label name
-> Instr (ToT (CtorOnlyField name dt) ': st) (ToT dt ': st)
instrWrapOne :: forall dt (name :: Symbol) (st :: [T]).
InstrWrapOneC dt name =>
Label name
-> Instr (ToT (CtorOnlyField name dt) : st) (ToT dt : st)
instrWrapOne Label name
_ =
forall (x :: * -> *) (path :: Path) (entryTy :: CtorField)
(s :: [T]).
GInstrWrap x path entryTy =>
Instr (AppendCtorField entryTy s) (GValueType x : s)
gInstrWrap @(GRep dt) @(LnrBranch (GetNamed name dt))
@(LnrFieldType (GetNamed name dt))
type InstrWrapC dt name =
( GenericIsoValue dt
, GInstrWrap (GRep dt)
(LnrBranch (GetNamed name dt))
(LnrFieldType (GetNamed name dt))
)
type InstrWrapOneC dt name =
( InstrWrapC dt name
, GetCtorField dt name ~ 'OneField (CtorOnlyField name dt)
)
hsWrap
:: forall dt name.
InstrWrapC dt name
=> Label name
-> ExtractCtorField (GetCtorField dt name)
-> dt
hsWrap :: forall dt (name :: Symbol).
InstrWrapC dt name =>
Label name -> ExtractCtorField (GetCtorField dt name) -> dt
hsWrap Label name
_ =
Rep dt Any -> dt
forall a x. Generic a => Rep a x -> a
forall x. Rep dt x -> dt
G.to (Rep dt Any -> dt)
-> (ExtractCtorField
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
-> Rep dt Any)
-> ExtractCtorField
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
-> dt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (x :: * -> *) (path :: Path) (entryTy :: CtorField) p.
GInstrWrap x path entryTy =>
ExtractCtorField entryTy -> x p
gHsWrap @(GRep dt) @(LnrBranch (GetNamed name dt))
@(LnrFieldType (GetNamed name dt))
class
GInstrWrap
(x :: Type -> Type)
(path :: Path)
(entryTy :: CtorField) where
gInstrWrap
:: Instr (AppendCtorField entryTy s) (GValueType x ': s)
gHsWrap
:: ExtractCtorField entryTy -> x p
instance GInstrWrap x path e => GInstrWrap (G.D1 i x) path e where
gInstrWrap :: forall (s :: [T]).
Instr (AppendCtorField e s) (GValueType (D1 i x) : s)
gInstrWrap = forall (x :: * -> *) (path :: Path) (entryTy :: CtorField)
(s :: [T]).
GInstrWrap x path entryTy =>
Instr (AppendCtorField entryTy s) (GValueType x : s)
gInstrWrap @x @path @e
gHsWrap :: forall p. 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 (x :: * -> *) (path :: Path) (entryTy :: CtorField) p.
GInstrWrap x path entryTy =>
ExtractCtorField entryTy -> x p
gHsWrap @x @path @e
instance (GInstrWrap x path e, SingI (GValueType y)) =>
GInstrWrap (x :+: y) ('L ': path) e where
gInstrWrap :: forall (s :: [T]).
Instr (AppendCtorField e s) (GValueType (x :+: y) : s)
gInstrWrap = forall (x :: * -> *) (path :: Path) (entryTy :: CtorField)
(s :: [T]).
GInstrWrap x path entryTy =>
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 (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (GValueType x : s) ('TOr (GValueType x) (GValueType y) : s)
forall {inp :: [T]} {out :: [T]} (b :: T) (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ ('TOr a b : s), SingI b) =>
Instr inp out
LEFT
gHsWrap :: forall p. 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 (x :: * -> *) (path :: Path) (entryTy :: CtorField) p.
GInstrWrap x path entryTy =>
ExtractCtorField entryTy -> x p
gHsWrap @x @path @e
instance (GInstrWrap y path e, SingI (GValueType x)) =>
GInstrWrap (x :+: y) ('R ': path) e where
gInstrWrap :: forall (s :: [T]).
Instr (AppendCtorField e s) (GValueType (x :+: y) : s)
gInstrWrap = forall (x :: * -> *) (path :: Path) (entryTy :: CtorField)
(s :: [T]).
GInstrWrap x path entryTy =>
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 (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (GValueType y : s) ('TOr (GValueType x) (GValueType y) : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (b : s), out ~ ('TOr a b : s), SingI a) =>
Instr inp out
RIGHT
gHsWrap :: forall p. 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 (x :: * -> *) (path :: Path) (entryTy :: CtorField) p.
GInstrWrap x path entryTy =>
ExtractCtorField entryTy -> x p
gHsWrap @y @path @e
instance GInstrWrap (G.C1 c (G.S1 i (G.Rec0 e))) '[ 'S] ('OneField e) where
gInstrWrap :: forall (s :: [T]).
Instr
(AppendCtorField ('OneField e) s)
(GValueType (C1 c (S1 i (Rec0 e))) : s)
gInstrWrap = Instr (ToT e : s) (ToT e : s)
Instr
(AppendCtorField ('OneField e) s)
(GValueType (C1 c (S1 i (Rec0 e))) : s)
forall (inp :: [T]). Instr inp inp
Nop
gHsWrap :: forall p. ExtractCtorField ('OneField e) -> C1 c (S1 i (Rec0 e)) p
gHsWrap = S1 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 (S1 i (Rec0 e) p -> C1 c (S1 i (Rec0 e)) p)
-> (e -> S1 i (Rec0 e) p) -> e -> C1 c (S1 i (Rec0 e)) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec0 e p -> S1 i (Rec0 e) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (Rec0 e p -> S1 i (Rec0 e) p)
-> (e -> Rec0 e p) -> e -> S1 i (Rec0 e) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Rec0 e p
forall k i c (p :: k). c -> K1 i c p
G.K1
instance ( path ~ (x ': xs)
, GInstrWrap (GRep sub) path e
, GenericIsoValue sub
) =>
GInstrWrap (G.C1 c (G.S1 i (G.Rec0 sub))) ('S ': x ': xs) e where
gInstrWrap :: forall (s :: [T]).
Instr
(AppendCtorField e s) (GValueType (C1 c (S1 i (Rec0 sub))) : s)
gInstrWrap = forall (x :: * -> *) (path :: Path) (entryTy :: CtorField)
(s :: [T]).
GInstrWrap x path entryTy =>
Instr (AppendCtorField entryTy s) (GValueType x : s)
gInstrWrap @(GRep sub) @path @e
gHsWrap :: forall p. ExtractCtorField e -> C1 c (S1 i (Rec0 sub)) p
gHsWrap = S1 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 (S1 i (Rec0 sub) p -> C1 c (S1 i (Rec0 sub)) p)
-> (ExtractCtorField e -> S1 i (Rec0 sub) p)
-> ExtractCtorField e
-> C1 c (S1 i (Rec0 sub)) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec0 sub p -> S1 i (Rec0 sub) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (Rec0 sub p -> S1 i (Rec0 sub) p)
-> (ExtractCtorField e -> Rec0 sub p)
-> ExtractCtorField e
-> S1 i (Rec0 sub) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sub -> Rec0 sub p
forall k i c (p :: k). c -> K1 i c p
G.K1 (sub -> Rec0 sub p)
-> (ExtractCtorField e -> sub) -> ExtractCtorField e -> Rec0 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
forall x. Rep sub x -> sub
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 (x :: * -> *) (path :: Path) (entryTy :: CtorField) p.
GInstrWrap x path entryTy =>
ExtractCtorField entryTy -> x p
gHsWrap @(GRep sub) @path @e
instance GInstrWrap (G.C1 c G.U1) '[ 'S] 'NoFields where
gInstrWrap :: forall (s :: [T]).
Instr (AppendCtorField 'NoFields s) (GValueType (C1 c U1) : s)
gInstrWrap = Value' Instr 'TUnit -> Instr s ('TUnit : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value' Instr 'TUnit
forall (instr :: [T] -> [T] -> *). Value' instr 'TUnit
VUnit
gHsWrap :: forall p. ExtractCtorField 'NoFields -> C1 c U1 p
gHsWrap () = U1 p -> M1 C 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
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
$cfrom :: forall x. MyType -> Rep MyType x
from :: forall x. MyType -> Rep MyType x
$cto :: forall x. Rep MyType x -> MyType
to :: forall x. Rep MyType x -> MyType
Generic
deriving anyclass WellTypedToT MyType
WellTypedToT MyType
-> (MyType -> Value (ToT MyType))
-> (Value (ToT MyType) -> MyType)
-> IsoValue MyType
Value (ToT MyType) -> MyType
MyType -> Value (ToT MyType)
forall a.
WellTypedToT a
-> (a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
$ctoVal :: MyType -> Value (ToT MyType)
toVal :: MyType -> Value (ToT MyType)
$cfromVal :: Value (ToT MyType) -> MyType
fromVal :: Value (ToT MyType) -> 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]
'LNR ('OneField Integer) '[ 'L, 'S]
:~: '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]
'LNR ('OneField ()) '[ 'R, 'L, 'S]
:~: 'LNR ('OneField ()) '[ 'R, 'L, 'S]
forall {k} (a :: k). a :~: a
Refl
_wrapMyType1 :: Instr (ToT Integer ': s) (ToT MyType ': s)
_wrapMyType1 :: forall (s :: [T]). Instr (ToT Integer : s) (ToT MyType : s)
_wrapMyType1 = forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyType Label "cMyCtor"
#cMyCtor
_wrapMyType1' :: Instr (ToT Integer ': s) (ToT MyType ': s)
_wrapMyType1' :: forall (s :: [T]). Instr (ToT Integer : s) (ToT MyType : s)
_wrapMyType1' = 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 :: forall (s :: [T]). Instr (ToT () : s) (ToT MyType : s)
_wrapMyType2 = forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyType Label "cComplexThing"
#cComplexThing
_wrapMyType3 :: Instr (ToT (ByteString, ()) ': s) (ToT MyType ': s)
_wrapMyType3 :: forall (s :: [T]).
Instr (ToT (ByteString, ()) : s) (ToT MyType : s)
_wrapMyType3 = forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyType 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
$cfrom :: forall x. MyType' -> Rep MyType' x
from :: forall x. MyType' -> Rep MyType' x
$cto :: forall x. Rep MyType' x -> MyType'
to :: forall x. Rep MyType' x -> MyType'
Generic
deriving anyclass WellTypedToT MyType'
WellTypedToT MyType'
-> (MyType' -> Value (ToT MyType'))
-> (Value (ToT MyType') -> MyType')
-> IsoValue MyType'
Value (ToT MyType') -> MyType'
MyType' -> Value (ToT MyType')
forall a.
WellTypedToT a
-> (a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
$ctoVal :: MyType' -> Value (ToT MyType')
toVal :: MyType' -> Value (ToT MyType')
$cfromVal :: Value (ToT MyType') -> MyType'
fromVal :: Value (ToT MyType') -> 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]
'LNR ('OneField Bool) '[ 'S] :~: 'LNR ('OneField Bool) '[ 'S]
forall {k} (a :: k). a :~: a
Refl
_wrapMyType' :: Instr (ToT Bool ': s) (ToT MyType' ': s)
_wrapMyType' :: forall (s :: [T]). Instr (ToT Bool : s) (ToT MyType' : s)
_wrapMyType' = forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyType' 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
$cfrom :: forall x. MyCompoundType -> Rep MyCompoundType x
from :: forall x. MyCompoundType -> Rep MyCompoundType x
$cto :: forall x. Rep MyCompoundType x -> MyCompoundType
to :: forall x. Rep MyCompoundType x -> MyCompoundType
Generic
deriving anyclass WellTypedToT MyCompoundType
WellTypedToT MyCompoundType
-> (MyCompoundType -> Value (ToT MyCompoundType))
-> (Value (ToT MyCompoundType) -> MyCompoundType)
-> IsoValue MyCompoundType
Value (ToT MyCompoundType) -> MyCompoundType
MyCompoundType -> Value (ToT MyCompoundType)
forall a.
WellTypedToT a
-> (a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
$ctoVal :: MyCompoundType -> Value (ToT MyCompoundType)
toVal :: MyCompoundType -> Value (ToT MyCompoundType)
$cfromVal :: Value (ToT MyCompoundType) -> MyCompoundType
fromVal :: Value (ToT MyCompoundType) -> 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]
'LNR ('OneField MyType) '[ 'L, 'L, 'S]
:~: '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]
'LNR ('OneField Integer) '[ 'L, 'L, 'S, 'L, 'S]
:~: '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]
'LNR ('OneField Integer) '[ 'L, 'R, 'S]
:~: '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]
'LNR ('OneField MyType') '[ 'R, 'R, 'S]
:~: '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]
'LNR ('OneField Bool) '[ 'R, 'R, 'S, 'S]
:~: 'LNR ('OneField Bool) '[ 'R, 'R, 'S, 'S]
forall {k} (a :: k). a :~: a
Refl
_wrapMyCompoundType1 :: Instr (ToT Integer ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType1 :: forall (s :: [T]). Instr (ToT Integer : s) (ToT MyCompoundType : s)
_wrapMyCompoundType1 = forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyCompoundType Label "cMyCtor"
#cMyCtor
_wrapMyCompoundType2 :: Instr (ToT Integer ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType2 :: forall (s :: [T]). Instr (ToT Integer : s) (ToT MyCompoundType : s)
_wrapMyCompoundType2 = forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyCompoundType Label "cCompoundPart2"
#cCompoundPart2
_wrapMyCompoundType3 :: Instr (ToT Bool ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType3 :: forall (s :: [T]). Instr (ToT Bool : s) (ToT MyCompoundType : s)
_wrapMyCompoundType3 = forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyCompoundType Label "cWrapBool"
#cWrapBool
_wrapMyCompoundType4 :: Instr (ToT MyType' ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType4 :: forall (s :: [T]). Instr (ToT MyType' : s) (ToT MyCompoundType : s)
_wrapMyCompoundType4 = forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyCompoundType 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
$cfrom :: forall x. MyEnum -> Rep MyEnum x
from :: forall x. MyEnum -> Rep MyEnum x
$cto :: forall x. Rep MyEnum x -> MyEnum
to :: forall x. Rep MyEnum x -> MyEnum
Generic
deriving anyclass WellTypedToT MyEnum
WellTypedToT MyEnum
-> (MyEnum -> Value (ToT MyEnum))
-> (Value (ToT MyEnum) -> MyEnum)
-> IsoValue MyEnum
Value (ToT MyEnum) -> MyEnum
MyEnum -> Value (ToT MyEnum)
forall a.
WellTypedToT a
-> (a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
$ctoVal :: MyEnum -> Value (ToT MyEnum)
toVal :: MyEnum -> Value (ToT MyEnum)
$cfromVal :: Value (ToT MyEnum) -> MyEnum
fromVal :: Value (ToT MyEnum) -> MyEnum
IsoValue
_wrapMyEnum1 :: Instr s (ToT MyEnum ': s)
_wrapMyEnum1 :: forall (s :: [T]). Instr s (ToT MyEnum : s)
_wrapMyEnum1 = forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyEnum Label "cCase1"
#cCase1
_wrapMyEnum2 :: Instr (ToT Integer ': s) (ToT MyEnum ': s)
_wrapMyEnum2 :: forall (s :: [T]). Instr (ToT Integer : s) (ToT MyEnum : s)
_wrapMyEnum2 = forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyEnum 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
$cfrom :: forall x. MyTypeWithNamedField -> Rep MyTypeWithNamedField x
from :: forall x. MyTypeWithNamedField -> Rep MyTypeWithNamedField x
$cto :: forall x. Rep MyTypeWithNamedField x -> MyTypeWithNamedField
to :: forall x. Rep MyTypeWithNamedField x -> MyTypeWithNamedField
Generic
deriving anyclass WellTypedToT MyTypeWithNamedField
WellTypedToT MyTypeWithNamedField
-> (MyTypeWithNamedField -> Value (ToT MyTypeWithNamedField))
-> (Value (ToT MyTypeWithNamedField) -> MyTypeWithNamedField)
-> IsoValue MyTypeWithNamedField
Value (ToT MyTypeWithNamedField) -> MyTypeWithNamedField
MyTypeWithNamedField -> Value (ToT MyTypeWithNamedField)
forall a.
WellTypedToT a
-> (a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
$ctoVal :: MyTypeWithNamedField -> Value (ToT MyTypeWithNamedField)
toVal :: MyTypeWithNamedField -> Value (ToT MyTypeWithNamedField)
$cfromVal :: Value (ToT MyTypeWithNamedField) -> MyTypeWithNamedField
fromVal :: Value (ToT MyTypeWithNamedField) -> MyTypeWithNamedField
IsoValue
_accessMyTypeWithNamedField :: Instr (ToT Natural ': s) (ToT MyTypeWithNamedField ': s)
_accessMyTypeWithNamedField :: forall (s :: [T]).
Instr (ToT Natural : s) (ToT MyTypeWithNamedField : s)
_accessMyTypeWithNamedField = forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @MyTypeWithNamedField Label "cCtorWithNamedField"
#cCtorWithNamedField
instrCase
:: forall dt out inp.
InstrCaseC dt
=> Rec (CaseClause inp out) (CaseClauses dt) -> RemFail Instr (ToT dt ': inp) out
instrCase :: forall dt (out :: [T]) (inp :: [T]).
InstrCaseC dt =>
Rec (CaseClause inp out) (CaseClauses dt)
-> RemFail Instr (ToT dt : inp) out
instrCase = (RemFail Instr (GValueType (Rep dt) : inp) out,
Rec (CaseClause inp out) '[])
-> RemFail Instr (GValueType (Rep dt) : inp) out
forall a b. (a, b) -> a
fst ((RemFail Instr (GValueType (Rep dt) : inp) out,
Rec (CaseClause inp out) '[])
-> RemFail Instr (GValueType (Rep dt) : inp) out)
-> (Rec (CaseClause inp out) (GCaseClauses (Rep dt) '[])
-> (RemFail Instr (GValueType (Rep dt) : inp) out,
Rec (CaseClause inp out) '[]))
-> Rec (CaseClause inp out) (GCaseClauses (Rep dt) '[])
-> RemFail Instr (GValueType (Rep dt) : inp) out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (x :: * -> *) (rest :: [CaseClauseParam]) (inp :: [T])
(out :: [T]).
GInstrCase x rest =>
Rec (CaseClause inp out) (GCaseClauses x rest)
-> (RemFail Instr (GValueType x : inp) out,
Rec (CaseClause inp out) rest)
gInstrCase @(GRep dt) @'[]
type InstrCaseC dt = (GenericIsoValue dt, GInstrCase (GRep dt) '[])
data CaseClauseParam = CaseClauseParam Symbol CtorField
data CaseClause (inp :: [T]) (out :: [T]) (param :: CaseClauseParam) where
CaseClause
:: RemFail Instr (AppendCtorField x inp) out
-> CaseClause inp out ('CaseClauseParam ctor x)
(//->)
:: Label ("c" `AppendSymbol` ctor)
-> RemFail Instr (AppendCtorField x inp) out
-> CaseClause inp out ('CaseClauseParam ctor x)
//-> :: 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)
(//->) Label (AppendSymbol "c" ctor)
_ = 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 //->
type CaseClauses a = GCaseClauses (GRep a) '[]
class GInstrCase (x :: Type -> Type) (rest :: [CaseClauseParam]) where
type GCaseClauses x rest :: [CaseClauseParam]
gInstrCase
:: forall inp out.
Rec (CaseClause inp out) (GCaseClauses x rest)
-> (RemFail Instr (GValueType x ': inp) out, Rec (CaseClause inp out) rest)
instance GInstrCase x rest => GInstrCase (G.D1 i x) rest where
type GCaseClauses (G.D1 i x) rest = GCaseClauses x rest
gInstrCase :: forall (inp :: [T]) (out :: [T]).
Rec (CaseClause inp out) (GCaseClauses (D1 i x) rest)
-> (RemFail Instr (GValueType (D1 i x) : inp) out,
Rec (CaseClause inp out) rest)
gInstrCase = forall (x :: * -> *) (rest :: [CaseClauseParam]) (inp :: [T])
(out :: [T]).
GInstrCase x rest =>
Rec (CaseClause inp out) (GCaseClauses x rest)
-> (RemFail Instr (GValueType x : inp) out,
Rec (CaseClause inp out) rest)
gInstrCase @x @rest
instance (GInstrCase x (GCaseClauses y rest), GInstrCase y rest) =>
GInstrCase (x :+: y) rest where
type GCaseClauses (x :+: y) rest = GCaseClauses x (GCaseClauses y rest)
gInstrCase :: forall (inp :: [T]) (out :: [T]).
Rec (CaseClause inp out) (GCaseClauses (x :+: y) rest)
-> (RemFail Instr (GValueType (x :+: y) : inp) out,
Rec (CaseClause inp out) rest)
gInstrCase Rec (CaseClause inp out) (GCaseClauses (x :+: y) rest)
clauses
| (RemFail Instr (GValueType x : inp) out
lres, Rec (CaseClause inp out) (GCaseClauses y rest)
rest) <- forall (x :: * -> *) (rest :: [CaseClauseParam]) (inp :: [T])
(out :: [T]).
GInstrCase x rest =>
Rec (CaseClause inp out) (GCaseClauses x rest)
-> (RemFail Instr (GValueType x : inp) out,
Rec (CaseClause inp out) rest)
gInstrCase @x Rec (CaseClause inp out) (GCaseClauses x (GCaseClauses y rest))
Rec (CaseClause inp out) (GCaseClauses (x :+: y) rest)
clauses
, (RemFail Instr (GValueType y : inp) out
rres, Rec (CaseClause inp out) rest
rest') <- forall (x :: * -> *) (rest :: [CaseClauseParam]) (inp :: [T])
(out :: [T]).
GInstrCase x rest =>
Rec (CaseClause inp out) (GCaseClauses x rest)
-> (RemFail Instr (GValueType x : inp) out,
Rec (CaseClause inp out) rest)
gInstrCase @y Rec (CaseClause inp out) (GCaseClauses y rest)
rest
= ((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 Instr (GValueType x : inp) o'
-> Instr (GValueType y : inp) o'
-> Instr ('TOr (GValueType x) (GValueType y) : inp) o'
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]) (out :: [T]) (b :: T).
Instr (a : s) out -> Instr (b : s) out -> Instr ('TOr a b : s) out
IF_LEFT RemFail Instr (GValueType x : inp) out
lres RemFail Instr (GValueType y : inp) out
rres, Rec (CaseClause inp out) rest
rest')
instance GInstrCase G.V1 rest where
type GCaseClauses G.V1 rest = rest
gInstrCase :: forall (inp :: [T]) (out :: [T]).
Rec (CaseClause inp out) (GCaseClauses V1 rest)
-> (RemFail Instr (GValueType V1 : inp) out,
Rec (CaseClause inp out) rest)
gInstrCase Rec (CaseClause inp out) (GCaseClauses V1 rest)
rest = ((forall (o' :: [T]). Instr ('TNever : inp) o')
-> RemFail Instr ('TNever : inp) out
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
(forall (o' :: k). instr i o') -> RemFail instr i o
RfAlwaysFails Instr ('TNever : inp) o'
forall (o' :: [T]). Instr ('TNever : inp) o'
forall (s :: [T]) (out :: [T]). Instr ('TNever : s) out
NEVER, Rec (CaseClause inp out) rest
Rec (CaseClause inp out) (GCaseClauses V1 rest)
rest)
instance GInstrCaseBranch ctor x => GInstrCase (G.C1 ('G.MetaCons ctor _1 _2) x) rest where
type GCaseClauses (G.C1 ('G.MetaCons ctor _1 _2) x) rest = GCaseBranchInput ctor x ': rest
gInstrCase :: forall (inp :: [T]) (out :: [T]).
Rec
(CaseClause inp out)
(GCaseClauses (C1 ('MetaCons ctor _1 _2) x) rest)
-> (RemFail
Instr (GValueType (C1 ('MetaCons ctor _1 _2) x) : inp) out,
Rec (CaseClause inp out) rest)
gInstrCase (CaseClause inp out r
clause :& Rec (CaseClause inp out) rs
rest) = (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, Rec (CaseClause inp out) rest
Rec (CaseClause inp out) rs
rest)
class GInstrCaseBranch (ctor :: Symbol) (x :: Type -> Type) where
type GCaseBranchInput ctor x :: CaseClauseParam
gInstrCaseBranch
:: CaseClause inp out (GCaseBranchInput ctor x)
-> RemFail Instr (GValueType x ': inp) out
instance
( TypeError ('Text "Cannot pattern match on constructors with more than 1 field"
':$$: 'Text "Consider using tuples instead")
, Bottom
) => GInstrCaseBranch ctor (x :*: y) where
type GCaseBranchInput ctor (x :*: y) = 'CaseClauseParam ctor 'NoFields
gInstrCaseBranch :: forall (inp :: [T]) (out :: [T]).
CaseClause inp out (GCaseBranchInput ctor (x :*: y))
-> RemFail Instr (GValueType (x :*: y) : inp) out
gInstrCaseBranch = forall a. Bottom => a
CaseClause inp out (GCaseBranchInput ctor (x :*: y))
-> RemFail Instr (GValueType (x :*: y) : inp) out
CaseClause inp out ('CaseClauseParam ctor 'NoFields)
-> RemFail Instr ('TPair (GValueType x) (GValueType y) : inp) out
forall a. a
no
instance GInstrCaseBranch ctor x => GInstrCaseBranch ctor (G.S1 i x) where
type GCaseBranchInput ctor (G.S1 i x) = GCaseBranchInput ctor x
gInstrCaseBranch :: forall (inp :: [T]) (out :: [T]).
CaseClause inp out (GCaseBranchInput ctor (S1 i x))
-> RemFail Instr (GValueType (S1 i x) : inp) out
gInstrCaseBranch = 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 GInstrCaseBranch ctor (G.Rec0 a) where
type GCaseBranchInput ctor (G.Rec0 a) = 'CaseClauseParam ctor ('OneField a)
gInstrCaseBranch :: forall (inp :: [T]) (out :: [T]).
CaseClause inp out (GCaseBranchInput ctor (Rec0 a))
-> RemFail Instr (GValueType (Rec0 a) : inp) out
gInstrCaseBranch (CaseClause 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 :: forall (inp :: [T]) (out :: [T]).
CaseClause inp out (GCaseBranchInput ctor U1)
-> RemFail Instr (GValueType U1 : inp) out
gInstrCaseBranch (CaseClause 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) (out :: [T]). Instr (a : out) out
DROP Instr ('TUnit : inp) inp -> Instr inp o' -> Instr ('TUnit : inp) o'
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq`) RemFail Instr inp out
RemFail Instr (AppendCtorField x inp) out
i
_caseMyType :: RemFail Instr (ToT MyType ': s) (ToT Integer ': s)
_caseMyType :: forall (s :: [T]). RemFail Instr (ToT MyType : s) (ToT Integer : s)
_caseMyType = 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 (ToT Integer : s)) (CaseClauses MyType)
-> RemFail Instr (ToT MyType : s) (ToT Integer : s))
-> Rec (CaseClause s (ToT Integer : 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
_caseMyType2 :: RemFail Instr (ToT MyType ': s) (ToT Integer ': s)
_caseMyType2 :: forall (s :: [T]). RemFail Instr (ToT MyType : s) (ToT Integer : s)
_caseMyType2 = 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 (ToT Integer : s)) (CaseClauses MyType)
-> RemFail Instr (ToT MyType : s) (ToT Integer : s))
-> Rec (CaseClause s (ToT Integer : 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
( 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 (inp :: [T]). Instr inp inp
Nop
, 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) (out :: [T]). Instr (a : out) out
DROP Instr ('TUnit : s) s
-> Instr s ('TInt : s) -> Instr ('TUnit : s) ('TInt : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Value' Instr 'TInt -> Instr s ('TInt : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH (forall a. IsoValue a => a -> Value (ToT a)
toVal @Integer Integer
5))
, 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) (out :: [T]). Instr (a : out) out
DROP Instr ('TPair 'TBytes 'TUnit : s) s
-> Instr s ('TInt : s)
-> Instr ('TPair 'TBytes 'TUnit : s) ('TInt : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Value' Instr 'TInt -> Instr s ('TInt : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH (forall a. IsoValue a => a -> Value (ToT a)
toVal @Integer Integer
0))
)
_caseMyEnum :: RemFail Instr (ToT MyEnum ': ToT Integer ': s) (ToT Integer ': s)
_caseMyEnum :: forall (s :: [T]).
RemFail Instr (ToT MyEnum : ToT Integer : s) (ToT Integer : s)
_caseMyEnum = forall dt (out :: [T]) (inp :: [T]).
InstrCaseC dt =>
Rec (CaseClause inp out) (CaseClauses dt)
-> RemFail Instr (ToT dt : inp) out
instrCase @MyEnum (Rec
(CaseClause (ToT Integer : s) (ToT Integer : s))
(CaseClauses MyEnum)
-> RemFail Instr (ToT MyEnum : ToT Integer : s) (ToT Integer : s))
-> Rec
(CaseClause (ToT Integer : s) (ToT Integer : 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
( 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) (out :: [T]). Instr (a : out) out
DROP Instr ('TInt : s) s
-> Instr s ('TInt : s) -> Instr ('TInt : s) ('TInt : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Value' Instr 'TInt -> Instr s ('TInt : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH (forall a. IsoValue a => a -> Value (ToT a)
toVal @Integer Integer
1))
, 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) (out :: [T]). Instr (a : out) out
DROP Instr ('TInt : s) s
-> Instr s ('TInt : s) -> Instr ('TInt : s) ('TInt : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Value' Instr 'TInt -> Instr s ('TInt : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH (forall a. IsoValue a => a -> Value (ToT a)
toVal @Integer Integer
2))
, 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) (out :: [T]). Instr (a : out) out
DROP Instr ('TInt : 'TInt : s) ('TInt : s)
-> Instr ('TInt : s) ('TInt : s)
-> Instr ('TInt : 'TInt : s) ('TInt : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr ('TInt : s) ('TInt : s)
forall (inp :: [T]). Instr inp inp
Nop)
, 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 (inp :: [T]). Instr inp inp
Nop
)
unsafeInstrUnwrap
:: forall dt name st.
InstrUnwrapC dt name
=> Label name
-> Instr (ToT dt ': st)
(ToT (CtorOnlyField name dt) ': st)
unsafeInstrUnwrap :: forall dt (name :: Symbol) (st :: [T]).
InstrUnwrapC dt name =>
Label name
-> Instr (ToT dt : st) (ToT (CtorOnlyField name dt) : st)
unsafeInstrUnwrap Label name
_ =
forall (x :: * -> *) (path :: Path) entryTy (s :: [T]).
GInstrUnwrap x path entryTy =>
Instr (GValueType x : s) (ToT entryTy : s)
unsafeGInstrUnwrap @(GRep dt) @(LnrBranch (GetNamed name dt))
@(CtorOnlyField name dt)
type InstrUnwrapC dt name =
( GenericIsoValue dt
, GInstrUnwrap (GRep dt)
(LnrBranch (GetNamed name dt))
(CtorOnlyField name dt)
)
hsUnwrap
:: forall dt name.
InstrUnwrapC dt name
=> Label name
-> dt
-> Maybe (CtorOnlyField name dt)
hsUnwrap :: forall dt (name :: Symbol).
InstrUnwrapC dt name =>
Label name -> dt -> Maybe (CtorOnlyField name dt)
hsUnwrap Label name
_ =
forall (x :: * -> *) (path :: Path) entryTy p.
GInstrUnwrap x path entryTy =>
x p -> Maybe entryTy
gHsUnwrap @(GRep dt) @(LnrBranch (GetNamed name dt))
@(CtorOnlyField name dt) (Rep dt Any
-> Maybe
(RequireOneField
name
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))))
-> (dt -> Rep dt Any)
-> dt
-> Maybe
(RequireOneField
name
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
dt -> Rep dt Any
forall x. dt -> Rep dt x
forall a x. Generic a => a -> Rep a x
G.from
class GInstrUnwrap
(x :: Type -> Type)
(path :: Path)
(entryTy :: Type) where
unsafeGInstrUnwrap
:: 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
unsafeGInstrUnwrap :: forall (s :: [T]). Instr (GValueType (D1 i x) : s) (ToT e : s)
unsafeGInstrUnwrap = forall (x :: * -> *) (path :: Path) entryTy (s :: [T]).
GInstrUnwrap x path entryTy =>
Instr (GValueType x : s) (ToT entryTy : s)
unsafeGInstrUnwrap @x @path @e
gHsUnwrap :: forall p. D1 i x p -> Maybe e
gHsUnwrap = 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 k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1
instance (GInstrUnwrap x path e, SingI (GValueType y)) =>
GInstrUnwrap (x :+: y) ('L ': path) e where
unsafeGInstrUnwrap :: forall (s :: [T]). Instr (GValueType (x :+: y) : s) (ToT e : s)
unsafeGInstrUnwrap = 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]) (out :: [T]) (b :: T).
Instr (a : s) out -> Instr (b : s) out -> Instr ('TOr a b : s) out
IF_LEFT (forall (x :: * -> *) (path :: Path) entryTy (s :: [T]).
GInstrUnwrap x path entryTy =>
Instr (GValueType x : s) (ToT entryTy : s)
unsafeGInstrUnwrap @x @path @e) Instr (GValueType y : s) (ToT e : s)
forall (i :: [T]) (o :: [T]). Instr i o
failWithWrongCtor
gHsUnwrap :: forall p. (:+:) x y p -> Maybe e
gHsUnwrap = \case
G.L1 x p
x -> forall (x :: * -> *) (path :: Path) entryTy p.
GInstrUnwrap x path entryTy =>
x p -> Maybe entryTy
gHsUnwrap @x @path @e x p
x
G.R1 y p
_ -> Maybe e
forall a. Maybe a
Nothing
instance (GInstrUnwrap y path e, SingI (GValueType x)) =>
GInstrUnwrap (x :+: y) ('R ': path) e where
unsafeGInstrUnwrap :: forall (s :: [T]). Instr (GValueType (x :+: y) : s) (ToT e : s)
unsafeGInstrUnwrap = 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]) (out :: [T]) (b :: T).
Instr (a : s) out -> Instr (b : s) out -> Instr ('TOr a b : s) out
IF_LEFT Instr (GValueType x : s) (ToT e : s)
forall (i :: [T]) (o :: [T]). Instr i o
failWithWrongCtor (forall (x :: * -> *) (path :: Path) entryTy (s :: [T]).
GInstrUnwrap x path entryTy =>
Instr (GValueType x : s) (ToT entryTy : s)
unsafeGInstrUnwrap @y @path @e)
gHsUnwrap :: forall p. (:+:) x y p -> Maybe e
gHsUnwrap = \case
G.R1 y p
y -> forall (x :: * -> *) (path :: Path) entryTy p.
GInstrUnwrap x path entryTy =>
x p -> Maybe entryTy
gHsUnwrap @y @path @e y p
y
G.L1 x p
_ -> Maybe e
forall a. Maybe a
Nothing
instance (IsoValue e) =>
GInstrUnwrap (G.C1 c (G.S1 i (G.Rec0 e))) '[ 'S] e where
unsafeGInstrUnwrap :: forall (s :: [T]).
Instr (GValueType (C1 c (S1 i (Rec0 e))) : s) (ToT e : s)
unsafeGInstrUnwrap = Instr (GValueType (C1 c (S1 i (Rec0 e))) : s) (ToT e : s)
Instr (ToT e : s) (ToT e : s)
forall (inp :: [T]). Instr inp inp
Nop
gHsUnwrap :: forall p. 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 k i c (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 k i (c :: Meta) (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 k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1
instance ( path ~ (x ': xs)
, GInstrUnwrap (GRep sub) path e
, GenericIsoValue sub
) =>
GInstrUnwrap (G.C1 c (G.S1 i (G.Rec0 sub))) ('S ': x ': xs) e where
unsafeGInstrUnwrap :: forall (s :: [T]).
Instr (GValueType (C1 c (S1 i (Rec0 sub))) : s) (ToT e : s)
unsafeGInstrUnwrap = forall (x :: * -> *) (path :: Path) entryTy (s :: [T]).
GInstrUnwrap x path entryTy =>
Instr (GValueType x : s) (ToT entryTy : s)
unsafeGInstrUnwrap @(GRep sub) @path @e
gHsUnwrap :: forall p. C1 c (S1 i (Rec0 sub)) p -> Maybe e
gHsUnwrap = forall (x :: * -> *) (path :: Path) entryTy p.
GInstrUnwrap x path entryTy =>
x p -> Maybe entryTy
gHsUnwrap @(GRep 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 x. sub -> Rep sub x
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 k i c (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 k i (c :: Meta) (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 k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1
failWithWrongCtor :: Instr i o
failWithWrongCtor :: forall (i :: [T]) (o :: [T]). Instr i o
failWithWrongCtor =
Value' Instr 'TString -> Instr i ('TString : i)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
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 (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq`
Instr ('TString : i) o
forall (a :: T) (s :: [T]) (out :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : s) out
FAILWITH
_unwrapMyType :: Instr (ToT MyType ': s) (ToT Integer ': s)
_unwrapMyType :: forall (s :: [T]). Instr (ToT MyType : s) (ToT Integer : s)
_unwrapMyType = forall dt (name :: Symbol) (st :: [T]).
InstrUnwrapC dt name =>
Label name
-> Instr (ToT dt : st) (ToT (CtorOnlyField name dt) : st)
unsafeInstrUnwrap @MyType Label "cMyCtor"
#cMyCtor
_unwrapMyCompoundType :: Instr (ToT MyCompoundType ': s) (ToT Integer ': s)
_unwrapMyCompoundType :: forall (s :: [T]). Instr (ToT MyCompoundType : s) (ToT Integer : s)
_unwrapMyCompoundType = forall dt (name :: Symbol) (st :: [T]).
InstrUnwrapC dt name =>
Label name
-> Instr (ToT dt : st) (ToT (CtorOnlyField name dt) : st)
unsafeInstrUnwrap @MyCompoundType Label "cMyCtor"
#cMyCtor
_unwrapMyCompoundType2 :: Instr (ToT MyCompoundType ': s) (ToT Address ': s)
_unwrapMyCompoundType2 :: forall (s :: [T]). Instr (ToT MyCompoundType : s) (ToT Address : s)
_unwrapMyCompoundType2 = forall dt (name :: Symbol) (st :: [T]).
InstrUnwrapC dt name =>
Label name
-> Instr (ToT dt : st) (ToT (CtorOnlyField name dt) : st)
unsafeInstrUnwrap @MyCompoundType Label "cCompoundPart3"
#cCompoundPart3
_unwrapMyCompoundType3 :: Instr (ToT MyCompoundType ': s) (ToT Bool ': s)
_unwrapMyCompoundType3 :: forall (s :: [T]). Instr (ToT MyCompoundType : s) (ToT Bool : s)
_unwrapMyCompoundType3 = forall dt (name :: Symbol) (st :: [T]).
InstrUnwrapC dt name =>
Label name
-> Instr (ToT dt : st) (ToT (CtorOnlyField name dt) : st)
unsafeInstrUnwrap @MyCompoundType Label "cWrapBool"
#cWrapBool
_unwrapMyCompoundType4 :: Instr (ToT MyCompoundType ': s) (ToT MyType' ': s)
_unwrapMyCompoundType4 :: forall (s :: [T]). Instr (ToT MyCompoundType : s) (ToT MyType' : s)
_unwrapMyCompoundType4 = forall dt (name :: Symbol) (st :: [T]).
InstrUnwrapC dt name =>
Label name
-> Instr (ToT dt : st) (ToT (CtorOnlyField name dt) : st)
unsafeInstrUnwrap @MyCompoundType Label "cCompoundPart4"
#cCompoundPart4