{-# LANGUAGE FunctionalDependencies #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
module Lorentz.ADT
( HasField
, HasFieldOfType
, HasFieldsOfType
, NamedField (..)
, (:=)
, HasDupableGetters
, toField
, toFieldNamed
, getField
, getFieldNamed
, setField
, modifyField
, construct
, constructT
, constructStack
, deconstruct
, fieldCtor
, wrap_
, wrapOne
, case_
, caseT
, unsafeUnwrap_
, CaseTC
, CaseArrow (..)
, CaseClauseL (..)
, InstrConstructC
, ConstructorFieldTypes
, Rec (..)
, (:!)
, (:?)
, getFieldOpen
, setFieldOpen
) where
import Data.Vinyl.Core (RMap(..), Rec(..))
import GHC.Generics qualified as G
import GHC.TypeLits (AppendSymbol, Symbol)
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Constraints
import Morley.Michelson.Typed.Haskell.Instr
import Morley.Michelson.Typed.Haskell.Value
import Morley.Util.Label (Label)
import Morley.Util.Named
import Morley.Util.Type (type (++))
import Morley.Util.TypeTuple
type HasField dt fname =
( InstrGetFieldC dt fname
, InstrSetFieldC dt fname
)
type HasFieldOfType dt fname fieldTy =
( HasField dt fname
, GetFieldType dt fname ~ fieldTy
)
data NamedField = NamedField Symbol Type
type n := ty = 'NamedField n ty
infixr 0 :=
type family HasFieldsOfType (dt :: Type) (fs :: [NamedField])
:: Constraint where
HasFieldsOfType _ '[] = ()
HasFieldsOfType dt ((n := ty) ': fs) =
(HasFieldOfType dt n ty, HasFieldsOfType dt fs)
class HasDupableGetters a
instance {-# OVERLAPPABLE #-} Dupable a => HasDupableGetters a
toField
:: forall dt name st.
InstrGetFieldC dt name
=> Label name -> dt : st :-> GetFieldType dt name : st
toField :: forall dt (name :: Symbol) (st :: [*]).
InstrGetFieldC dt name =>
Label name -> (dt : st) :-> (GetFieldType dt name : st)
toField = Instr
(GValueType (Rep dt) : ToTs st)
(ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
: ToTs st)
-> (dt : st)
:-> (LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))
: st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
(GValueType (Rep dt) : ToTs st)
(ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
: ToTs st)
-> (dt : st)
:-> (LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))
: st))
-> (Label name
-> Instr
(GValueType (Rep dt) : ToTs st)
(ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
: ToTs st))
-> Label name
-> (dt : st)
:-> (LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))
: st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (name :: Symbol) (st :: [T]).
InstrGetFieldC dt name =>
Label name -> Instr (ToT dt : st) (ToT (GetFieldType dt name) : st)
instrToField @dt
toFieldNamed
:: forall dt name st.
InstrGetFieldC dt name
=> Label name -> dt : st :-> (name :! GetFieldType dt name) : st
toFieldNamed :: forall dt (name :: Symbol) (st :: [*]).
InstrGetFieldC dt name =>
Label name -> (dt : st) :-> ((name :! GetFieldType dt name) : st)
toFieldNamed Label name
l = Label name
-> (dt : st)
:-> (LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))
: st)
forall dt (name :: Symbol) (st :: [*]).
InstrGetFieldC dt name =>
Label name -> (dt : st) :-> (GetFieldType dt name : st)
toField Label name
l ((dt : st)
:-> (LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))
: st))
-> ((LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))
: st)
:-> (NamedF
Identity
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
name
: st))
-> (dt : st)
:-> (NamedF
Identity
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
name
: st)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label name
-> (LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))
: st)
:-> (NamedF
Identity
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
name
: st)
forall (name :: Symbol) a (s :: [*]).
Label name -> (a : s) :-> ((name :! a) : s)
toNamed Label name
l
getField
:: forall dt name st.
(InstrGetFieldC dt name, Dupable (GetFieldType dt name), HasDupableGetters dt)
=> Label name -> dt : st :-> GetFieldType dt name : dt ': st
getField :: forall dt (name :: Symbol) (st :: [*]).
(InstrGetFieldC dt name, Dupable (GetFieldType dt name),
HasDupableGetters dt) =>
Label name -> (dt : st) :-> (GetFieldType dt name : dt : st)
getField = Instr
(GValueType (Rep dt) : ToTs st)
(ToT (GetFieldType dt name) : GValueType (Rep dt) : ToTs st)
-> (dt : st) :-> (GetFieldType dt name : dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
(GValueType (Rep dt) : ToTs st)
(ToT (GetFieldType dt name) : GValueType (Rep dt) : ToTs st)
-> (dt : st) :-> (GetFieldType dt name : dt : st))
-> (Label name
-> Instr
(GValueType (Rep dt) : ToTs st)
(ToT (GetFieldType dt name) : GValueType (Rep dt) : ToTs st))
-> Label name
-> (dt : st) :-> (GetFieldType dt name : dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (name :: Symbol) (st :: [T]).
(InstrGetFieldC dt name,
DupableScope (ToT (GetFieldType dt name))) =>
Label name
-> Instr (ToT dt : st) (ToT (GetFieldType dt name) : ToT dt : st)
instrGetField @dt
where
_needHasDupableGetters :: Dict (HasDupableGetters dt)
_needHasDupableGetters = forall (a :: Constraint). a => Dict a
Dict @(HasDupableGetters dt)
getFieldNamed
:: forall dt name st.
(InstrGetFieldC dt name, Dupable (GetFieldType dt name), HasDupableGetters dt)
=> Label name -> dt : st :-> (name :! GetFieldType dt name) : dt ': st
getFieldNamed :: forall dt (name :: Symbol) (st :: [*]).
(InstrGetFieldC dt name, Dupable (GetFieldType dt name),
HasDupableGetters dt) =>
Label name
-> (dt : st) :-> ((name :! GetFieldType dt name) : dt : st)
getFieldNamed Label name
l = Label name -> (dt : st) :-> (GetFieldType dt name : dt : st)
forall dt (name :: Symbol) (st :: [*]).
(InstrGetFieldC dt name, Dupable (GetFieldType dt name),
HasDupableGetters dt) =>
Label name -> (dt : st) :-> (GetFieldType dt name : dt : st)
getField Label name
l ((dt : st) :-> (GetFieldType dt name : dt : st))
-> ((GetFieldType dt name : dt : st)
:-> ((name :! GetFieldType dt name) : dt : st))
-> (dt : st) :-> ((name :! GetFieldType dt name) : dt : st)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (GetFieldType dt name : dt : st)
:-> ((name :! GetFieldType dt name) : dt : st)
forall a (s :: [*]).
Wrappable a =>
(Unwrappabled a : s) :-> (a : s)
coerceWrap
setField
:: forall dt name st.
InstrSetFieldC dt name
=> Label name -> (GetFieldType dt name ': dt ': st) :-> (dt ': st)
setField :: forall dt (name :: Symbol) (st :: [*]).
InstrSetFieldC dt name =>
Label name -> (GetFieldType dt name : dt : st) :-> (dt : st)
setField = Instr
(ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
: GValueType (Rep dt) : ToTs st)
(GValueType (Rep dt) : ToTs st)
-> (LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))
: dt : st)
:-> (dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
(ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
: GValueType (Rep dt) : ToTs st)
(GValueType (Rep dt) : ToTs st)
-> (LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))
: dt : st)
:-> (dt : st))
-> (Label name
-> Instr
(ToT
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
: GValueType (Rep dt) : ToTs st)
(GValueType (Rep dt) : ToTs st))
-> Label name
-> (LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))
: dt : st)
:-> (dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (name :: Symbol) (st :: [T]).
InstrSetFieldC dt name =>
Label name
-> Instr (ToT (GetFieldType dt name) : ToT dt : st) (ToT dt : st)
instrSetField @dt
modifyField
:: forall dt name st.
( InstrGetFieldC dt name
, InstrSetFieldC dt name
, Dupable (GetFieldType dt name)
, HasDupableGetters dt
)
=> Label name
-> (forall st0. (GetFieldType dt name ': st0) :-> (GetFieldType dt name ': st0))
-> dt : st :-> dt : st
modifyField :: forall dt (name :: Symbol) (st :: [*]).
(InstrGetFieldC dt name, InstrSetFieldC dt name,
Dupable (GetFieldType dt name), HasDupableGetters dt) =>
Label name
-> (forall (st0 :: [*]).
(GetFieldType dt name : st0) :-> (GetFieldType dt name : st0))
-> (dt : st) :-> (dt : st)
modifyField Label name
l forall (st0 :: [*]).
(GetFieldType dt name : st0) :-> (GetFieldType dt name : st0)
i = forall dt (name :: Symbol) (st :: [*]).
(InstrGetFieldC dt name, Dupable (GetFieldType dt name),
HasDupableGetters dt) =>
Label name -> (dt : st) :-> (GetFieldType dt name : dt : st)
getField @dt Label name
l ((dt : st) :-> (GetFieldType dt name : dt : st))
-> ((GetFieldType dt name : dt : st)
:-> (GetFieldType dt name : dt : st))
-> (dt : st) :-> (GetFieldType dt name : dt : st)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (GetFieldType dt name : dt : st)
:-> (GetFieldType dt name : dt : st)
forall (st0 :: [*]).
(GetFieldType dt name : st0) :-> (GetFieldType dt name : st0)
i ((dt : st) :-> (GetFieldType dt name : dt : st))
-> ((GetFieldType dt name : dt : st) :-> (dt : st))
-> (dt : st) :-> (dt : st)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall dt (name :: Symbol) (st :: [*]).
InstrSetFieldC dt name =>
Label name -> (GetFieldType dt name : dt : st) :-> (dt : st)
setField @dt Label name
l
getFieldOpen
:: forall dt name res st.
(InstrGetFieldC dt name, HasDupableGetters dt)
=> '[GetFieldType dt name] :-> '[res, GetFieldType dt name]
-> '[GetFieldType dt name] :-> '[res]
-> Label name
-> dt : st :-> res : dt ': st
getFieldOpen :: forall dt (name :: Symbol) res (st :: [*]).
(InstrGetFieldC dt name, HasDupableGetters dt) =>
('[GetFieldType dt name] :-> '[res, GetFieldType dt name])
-> ('[GetFieldType dt name] :-> '[res])
-> Label name
-> (dt : st) :-> (res : dt : st)
getFieldOpen '[LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))]
:-> '[res,
LnrFieldType (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
contWDup '[LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))]
:-> '[res]
contWoDup =
Instr
(GValueType (Rep dt) : ToTs st)
(ToT res : GValueType (Rep dt) : ToTs st)
-> (dt : st) :-> (res : dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
(GValueType (Rep dt) : ToTs st)
(ToT res : GValueType (Rep dt) : ToTs st)
-> (dt : st) :-> (res : dt : st))
-> (Label name
-> Instr
(GValueType (Rep dt) : ToTs st)
(ToT res : GValueType (Rep dt) : ToTs st))
-> Label name
-> (dt : st) :-> (res : dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (name :: Symbol) (res :: T) (st :: [T]).
InstrGetFieldC dt name =>
Instr
'[ToT (GetFieldType dt name)] '[res, ToT (GetFieldType dt name)]
-> Instr '[ToT (GetFieldType dt name)] '[res]
-> Label name
-> Instr (ToT dt : st) (res : ToT dt : st)
instrGetFieldOpen @dt (('[LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))]
:-> '[res,
LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))])
-> Instr
(ToTs
'[LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))])
(ToTs
'[res,
LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))])
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iNonFailingCode '[LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))]
:-> '[res,
LnrFieldType (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
contWDup) (('[LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))]
:-> '[res])
-> Instr
(ToTs
'[LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))])
(ToTs '[res])
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iNonFailingCode '[LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))]
:-> '[res]
contWoDup)
where
_needHasDupableGetters :: Dict (HasDupableGetters dt)
_needHasDupableGetters = forall (a :: Constraint). a => Dict a
Dict @(HasDupableGetters dt)
setFieldOpen
:: forall dt name new st.
InstrSetFieldC dt name
=> '[new, GetFieldType dt name] :-> '[GetFieldType dt name]
-> Label name
-> (new ': dt ': st) :-> (dt ': st)
setFieldOpen :: forall dt (name :: Symbol) new (st :: [*]).
InstrSetFieldC dt name =>
('[new, GetFieldType dt name] :-> '[GetFieldType dt name])
-> Label name -> (new : dt : st) :-> (dt : st)
setFieldOpen '[new,
LnrFieldType (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
:-> '[LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))]
cont =
Instr
(ToT new : GValueType (Rep dt) : ToTs st)
(GValueType (Rep dt) : ToTs st)
-> (new : dt : st) :-> (dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
(ToT new : GValueType (Rep dt) : ToTs st)
(GValueType (Rep dt) : ToTs st)
-> (new : dt : st) :-> (dt : st))
-> (Label name
-> Instr
(ToT new : GValueType (Rep dt) : ToTs st)
(GValueType (Rep dt) : ToTs st))
-> Label name
-> (new : dt : st) :-> (dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (name :: Symbol) (new :: T) (st :: [T]).
InstrSetFieldC dt name =>
Instr
'[new, ToT (GetFieldType dt name)] '[ToT (GetFieldType dt name)]
-> Label name -> Instr (new : ToT dt : st) (ToT dt : st)
instrSetFieldOpen @dt (('[new,
LnrFieldType (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
:-> '[LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))])
-> Instr
(ToTs
'[new,
LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))])
(ToTs
'[LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))])
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iNonFailingCode '[new,
LnrFieldType (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
:-> '[LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))]
cont)
construct
:: forall dt st.
( InstrConstructC dt
, RMap (ConstructorFieldTypes dt)
)
=> Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> st :-> dt : st
construct :: forall dt (st :: [*]).
(InstrConstructC dt, RMap (ConstructorFieldTypes dt)) =>
Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> st :-> (dt : st)
construct Rec (FieldConstructor st) (ConstructorFieldTypes dt)
fctors =
Instr (ToTs st) (ToTs (dt : st)) -> st :-> (dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs st) (ToTs (dt : st)) -> st :-> (dt : st))
-> Instr (ToTs st) (ToTs (dt : st)) -> st :-> (dt : st)
forall a b. (a -> b) -> a -> b
$ forall dt (st :: [T]).
InstrConstructC dt =>
Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> Instr st (ToT dt : st)
instrConstruct @dt (Rec (FieldConstructor (ToTs st)) (ConstructorFieldTypes dt)
-> Instr (ToTs st) (ToT dt : ToTs st))
-> Rec (FieldConstructor (ToTs st)) (ConstructorFieldTypes dt)
-> Instr (ToTs st) (ToT dt : ToTs st)
forall a b. (a -> b) -> a -> b
$
(forall x. FieldConstructor st x -> FieldConstructor (ToTs st) x)
-> Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> Rec (FieldConstructor (ToTs st)) (ConstructorFieldTypes dt)
forall {u} (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap (\(FieldConstructor Instr (ToTs' st) (ToT x : ToTs' st)
i) -> Instr (ToTs' (ToTs st)) (ToT x : ToTs' (ToTs st))
-> FieldConstructor (ToTs st) x
forall k (st :: [k]) field.
Instr (ToTs' st) (ToT field : ToTs' st)
-> FieldConstructor st field
FieldConstructor Instr (ToTs' st) (ToT x : ToTs' st)
Instr (ToTs' (ToTs st)) (ToT x : ToTs' (ToTs st))
i) Rec (FieldConstructor st) (ConstructorFieldTypes dt)
fctors
constructT
:: forall dt fctors st.
( InstrConstructC dt
, RMap (ConstructorFieldTypes dt)
, fctors ~ Rec (FieldConstructor st) (ConstructorFieldTypes dt)
, RecFromTuple fctors
)
=> IsoRecTuple fctors
-> st :-> dt : st
constructT :: forall dt fctors (st :: [*]).
(InstrConstructC dt, RMap (ConstructorFieldTypes dt),
fctors ~ Rec (FieldConstructor st) (ConstructorFieldTypes dt),
RecFromTuple fctors) =>
IsoRecTuple fctors -> st :-> (dt : st)
constructT = Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> st :-> (dt : st)
forall dt (st :: [*]).
(InstrConstructC dt, RMap (ConstructorFieldTypes dt)) =>
Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> st :-> (dt : st)
construct (Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> st :-> (dt : st))
-> (IsoRecTuple
(Rec (FieldConstructor st) (ConstructorFieldTypes dt))
-> Rec (FieldConstructor st) (ConstructorFieldTypes dt))
-> IsoRecTuple
(Rec (FieldConstructor st) (ConstructorFieldTypes dt))
-> st :-> (dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsoRecTuple (Rec (FieldConstructor st) (ConstructorFieldTypes dt))
-> Rec (FieldConstructor st) (ConstructorFieldTypes dt)
forall r. RecFromTuple r => IsoRecTuple r -> r
recFromTuple
constructStack
:: forall dt fields st .
( InstrConstructC dt
, fields ~ ConstructorFieldTypes dt
, ToTs fields ++ ToTs st ~ ToTs (fields ++ st)
)
=> (fields ++ st) :-> dt : st
constructStack :: forall dt (fields :: [*]) (st :: [*]).
(InstrConstructC dt, fields ~ ConstructorFieldTypes dt,
(ToTs fields ++ ToTs st) ~ ToTs (fields ++ st)) =>
(fields ++ st) :-> (dt : st)
constructStack =
Instr (ToTs (fields ++ st)) (ToTs (dt : st))
-> (fields ++ st) :-> (dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (forall dt (stack :: [T]) (st :: [T]).
(InstrConstructC dt, stack ~ ToTs (ConstructorFieldTypes dt)) =>
Instr (stack ++ st) (ToT dt : st)
instrConstructStack @dt @(ToTs fields))
deconstruct
:: forall dt fields st .
( InstrDeconstructC dt (ToTs st)
, fields ~ GFieldTypes (G.Rep dt) '[]
, ToTs fields ++ ToTs st ~ ToTs (fields ++ st)
)
=> dt : st :-> (fields ++ st)
deconstruct :: forall dt (fields :: [*]) (st :: [*]).
(InstrDeconstructC dt (ToTs st), fields ~ GFieldTypes (Rep dt) '[],
(ToTs fields ++ ToTs st) ~ ToTs (fields ++ st)) =>
(dt : st) :-> (fields ++ st)
deconstruct =
Instr (ToTs (dt : st)) (ToTs (fields ++ st))
-> (dt : st) :-> (fields ++ st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (forall dt (stack :: [T]) (st :: [T]).
(InstrDeconstructC dt st,
stack ~ ToTs (GFieldTypes (Rep dt) '[])) =>
Instr (ToT dt : st) (stack ++ st)
instrDeconstruct @dt @(ToTs fields))
fieldCtor :: HasCallStack => (st :-> f : st) -> FieldConstructor st f
fieldCtor :: forall (st :: [*]) f.
HasCallStack =>
(st :-> (f : st)) -> FieldConstructor st f
fieldCtor = \case
I Instr (ToTs st) (ToTs (f : st))
i -> Instr (ToTs' st) (ToT f : ToTs' st) -> FieldConstructor st f
forall k (st :: [k]) field.
Instr (ToTs' st) (ToT field : ToTs' st)
-> FieldConstructor st field
FieldConstructor Instr (ToTs st) (ToTs (f : st))
Instr (ToTs' st) (ToT f : ToTs' st)
i
FI forall (out' :: [T]). Instr (ToTs st) out'
_ -> Text -> FieldConstructor st f
forall a. HasCallStack => Text -> a
error Text
"Field constructor always fails"
wrap_
:: forall dt name st.
InstrWrapC dt name
=> Label name -> (AppendCtorField (GetCtorField dt name) st) :-> dt : st
wrap_ :: forall dt (name :: Symbol) (st :: [*]).
InstrWrapC dt name =>
Label name
-> AppendCtorField (GetCtorField dt name) st :-> (dt : st)
wrap_ =
case forall (cf :: CtorField) (st :: [*]).
(AppendCtorFieldAxiom ('OneField Word) '[Int],
AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom @(GetCtorField dt name) @st of
Dict
(AppendCtorFieldAxiom
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
st)
Dict -> Instr
(ToTs
(AppendCtorField
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
st))
(GValueType (Rep dt) : ToTs st)
-> AppendCtorField
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
st
:-> (dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
(ToTs
(AppendCtorField
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
st))
(GValueType (Rep dt) : ToTs st)
-> AppendCtorField
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
st
:-> (dt : st))
-> (Label name
-> Instr
(ToTs
(AppendCtorField
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
st))
(GValueType (Rep dt) : ToTs st))
-> Label name
-> AppendCtorField
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
st
:-> (dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @dt
wrapOne
:: forall dt name st.
InstrWrapOneC dt name
=> Label name -> (CtorOnlyField name dt ': st) :-> dt : st
wrapOne :: forall dt (name :: Symbol) (st :: [*]).
InstrWrapOneC dt name =>
Label name -> (CtorOnlyField name dt : st) :-> (dt : st)
wrapOne = case forall (cf :: CtorField) (st :: [*]).
(AppendCtorFieldAxiom ('OneField Word) '[Int],
AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom @(GetCtorField dt name) @st of
Dict (AppendCtorFieldAxiom (GetCtorField dt name) st)
Dict -> Instr
(ToT (CtorOnlyField name dt) : ToTs st)
(GValueType (Rep dt) : ToTs st)
-> (CtorOnlyField name dt : st) :-> (dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
(ToT (CtorOnlyField name dt) : ToTs st)
(GValueType (Rep dt) : ToTs st)
-> (CtorOnlyField name dt : st) :-> (dt : st))
-> (Label name
-> Instr
(ToT (CtorOnlyField name dt) : ToTs st)
(GValueType (Rep dt) : ToTs st))
-> Label name
-> (CtorOnlyField name dt : st) :-> (dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (name :: Symbol) (st :: [T]).
InstrWrapOneC dt name =>
Label name
-> Instr (ToT (CtorOnlyField name dt) : st) (ToT dt : st)
instrWrapOne @dt
data CaseClauseL (inp :: [Type]) (out :: [Type]) (param :: CaseClauseParam) where
CaseClauseL :: AppendCtorField x inp :-> out -> CaseClauseL inp out ('CaseClauseParam ctor x)
class CaseArrow name body clause | clause -> name, clause -> body where
(/->) :: Label name -> body -> clause
infixr 0 /->
instance ( name ~ ("c" `AppendSymbol` ctor)
, body ~ (AppendCtorField x inp :-> out)
) => CaseArrow name body
(CaseClauseL inp out ('CaseClauseParam ctor x)) where
/-> :: Label name -> body -> CaseClauseL inp out ('CaseClauseParam ctor x)
(/->) Label name
_ = body -> CaseClauseL inp out ('CaseClauseParam ctor x)
forall (x :: CtorField) (inp :: [*]) (out :: [*]) (ctor :: Symbol).
(AppendCtorField x inp :-> out)
-> CaseClauseL inp out ('CaseClauseParam ctor x)
CaseClauseL
case_
:: forall dt out inp.
( InstrCaseC dt
, RMap (CaseClauses dt)
)
=> Rec (CaseClauseL inp out) (CaseClauses dt) -> dt : inp :-> out
case_ :: forall dt (out :: [*]) (inp :: [*]).
(InstrCaseC dt, RMap (CaseClauses dt)) =>
Rec (CaseClauseL inp out) (CaseClauses dt) -> (dt : inp) :-> out
case_ = RemFail Instr (GValueType (Rep dt) : ToTs inp) (ToTs out)
-> (dt : inp) :-> out
forall (inp :: [*]) (out :: [*]).
RemFail Instr (ToTs inp) (ToTs out) -> inp :-> out
LorentzInstr (RemFail Instr (GValueType (Rep dt) : ToTs inp) (ToTs out)
-> (dt : inp) :-> out)
-> (Rec (CaseClauseL inp out) (CaseClauses dt)
-> RemFail Instr (GValueType (Rep dt) : ToTs inp) (ToTs out))
-> Rec (CaseClauseL inp out) (CaseClauses dt)
-> (dt : inp) :-> out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (out :: [T]) (inp :: [T]).
InstrCaseC dt =>
Rec (CaseClause inp out) (CaseClauses dt)
-> RemFail Instr (ToT dt : inp) out
instrCase @dt (Rec (CaseClause (ToTs inp) (ToTs out)) (CaseClauses dt)
-> RemFail Instr (GValueType (Rep dt) : ToTs inp) (ToTs out))
-> (Rec (CaseClauseL inp out) (CaseClauses dt)
-> Rec (CaseClause (ToTs inp) (ToTs out)) (CaseClauses dt))
-> Rec (CaseClauseL inp out) (CaseClauses dt)
-> RemFail Instr (GValueType (Rep dt) : ToTs inp) (ToTs out)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: CaseClauseParam).
CaseClauseL inp out x -> CaseClause (ToTs inp) (ToTs out) x)
-> Rec (CaseClauseL inp out) (CaseClauses dt)
-> Rec (CaseClause (ToTs inp) (ToTs out)) (CaseClauses dt)
forall {u} (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap forall (x :: CaseClauseParam).
CaseClauseL inp out x -> CaseClause (ToTs inp) (ToTs out) x
coerceCaseClause
where
coerceCaseClause
:: forall clauses.
CaseClauseL inp out clauses -> CaseClause (ToTs inp) (ToTs out) clauses
coerceCaseClause :: forall (x :: CaseClauseParam).
CaseClauseL inp out x -> CaseClause (ToTs inp) (ToTs out) x
coerceCaseClause (CaseClauseL (LorentzInstr RemFail Instr (ToTs (AppendCtorField x inp)) (ToTs out)
cc)) =
RemFail Instr (AppendCtorField x (ToTs inp)) (ToTs out)
-> CaseClause (ToTs inp) (ToTs 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 (RemFail Instr (AppendCtorField x (ToTs inp)) (ToTs out)
-> CaseClause (ToTs inp) (ToTs out) ('CaseClauseParam ctor x))
-> RemFail Instr (AppendCtorField x (ToTs inp)) (ToTs out)
-> CaseClause (ToTs inp) (ToTs out) ('CaseClauseParam ctor x)
forall a b. (a -> b) -> a -> b
$ case forall {k} (t :: k). Proxy t
forall {t :: CaseClauseParam}. Proxy t
Proxy @clauses of
(Proxy ('CaseClauseParam ctor x)
_ :: Proxy ('CaseClauseParam ctor cc)) ->
case forall (cf :: CtorField) (st :: [*]).
(AppendCtorFieldAxiom ('OneField Word) '[Int],
AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom @cc @inp of Dict (AppendCtorFieldAxiom x inp)
Dict -> RemFail Instr (AppendCtorField x (ToTs inp)) (ToTs out)
RemFail Instr (ToTs (AppendCtorField x inp)) (ToTs out)
cc
caseT
:: forall dt out inp clauses.
CaseTC dt out inp clauses
=> IsoRecTuple clauses -> dt : inp :-> out
caseT :: forall dt (out :: [*]) (inp :: [*]) clauses.
CaseTC dt out inp clauses =>
IsoRecTuple clauses -> (dt : inp) :-> out
caseT = forall dt (out :: [*]) (inp :: [*]).
(InstrCaseC dt, RMap (CaseClauses dt)) =>
Rec (CaseClauseL inp out) (CaseClauses dt) -> (dt : inp) :-> out
case_ @dt (Rec (CaseClauseL inp out) (CaseClauses dt) -> (dt : inp) :-> out)
-> (IsoRecTuple (Rec (CaseClauseL inp out) (CaseClauses dt))
-> Rec (CaseClauseL inp out) (CaseClauses dt))
-> IsoRecTuple (Rec (CaseClauseL inp out) (CaseClauses dt))
-> (dt : inp) :-> out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsoRecTuple (Rec (CaseClauseL inp out) (CaseClauses dt))
-> Rec (CaseClauseL inp out) (CaseClauses dt)
forall r. RecFromTuple r => IsoRecTuple r -> r
recFromTuple
type CaseTC dt out inp clauses =
( InstrCaseC dt
, RMap (CaseClauses dt)
, RecFromTuple clauses
, clauses ~ Rec (CaseClauseL inp out) (CaseClauses dt)
)
unsafeUnwrap_
:: forall dt name st.
InstrUnwrapC dt name
=> Label name -> dt : st :-> (CtorOnlyField name dt ': st)
unsafeUnwrap_ :: forall dt (name :: Symbol) (st :: [*]).
InstrUnwrapC dt name =>
Label name -> (dt : st) :-> (CtorOnlyField name dt : st)
unsafeUnwrap_ =
case forall (cf :: CtorField) (st :: [*]).
(AppendCtorFieldAxiom ('OneField Word) '[Int],
AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom @(GetCtorField dt name) @st of
Dict
(AppendCtorFieldAxiom
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
st)
Dict -> Instr
(GValueType (Rep dt) : ToTs st)
(ToT
(RequireOneField
name
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))))
: ToTs st)
-> (dt : st)
:-> (RequireOneField
name
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
: st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
(GValueType (Rep dt) : ToTs st)
(ToT
(RequireOneField
name
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))))
: ToTs st)
-> (dt : st)
:-> (RequireOneField
name
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
: st))
-> (Label name
-> Instr
(GValueType (Rep dt) : ToTs st)
(ToT
(RequireOneField
name
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt)))))
: ToTs st))
-> Label name
-> (dt : st)
:-> (RequireOneField
name
(LnrFieldType
(LNRequireFound name dt (GLookupNamed name (Rep dt))))
: st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (name :: Symbol) (st :: [T]).
InstrUnwrapC dt name =>
Label name
-> Instr (ToT dt : st) (ToT (CtorOnlyField name dt) : st)
unsafeInstrUnwrap @dt