{-# 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.Constraint ((\\))
import Data.Vinyl.Core (RMap(..), Rec(..))
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 (KnownList, 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 :: Label name -> (dt : st) :-> (GetFieldType dt name : st)
toField = Instr
(GValueType (Rep dt) : ToTs st)
(ToT (GetFieldType dt name) : ToTs st)
-> (dt : st) :-> (GetFieldType dt name : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
(GValueType (Rep dt) : ToTs st)
(ToT (GetFieldType dt name) : ToTs st)
-> (dt : st) :-> (GetFieldType dt name : st))
-> (Label name
-> Instr
(GValueType (Rep dt) : ToTs st)
(ToT (GetFieldType dt name) : ToTs st))
-> Label name
-> (dt : st) :-> (GetFieldType dt name : 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)
forall (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 :: Label name -> (dt : st) :-> ((name :! GetFieldType dt name) : st)
toFieldNamed Label name
l = Label name -> (dt : st) :-> (GetFieldType dt name : st)
forall dt (name :: Symbol) (st :: [*]).
InstrGetFieldC dt name =>
Label name -> (dt : st) :-> (GetFieldType dt name : st)
toField Label name
l ((dt : st) :-> (GetFieldType dt name : st))
-> ((GetFieldType dt name : st)
:-> ((name :! GetFieldType dt name) : st))
-> (dt : st) :-> ((name :! GetFieldType dt name) : st)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label name
-> (GetFieldType dt name : st)
:-> ((name :! GetFieldType 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 :: 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)
forall (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
(DupableScope (ToT (GetFieldType dt name)) =>
Label name -> (dt : st) :-> (GetFieldType dt name : dt : st))
-> (((SingI (ToT (GetFieldType dt name)),
FailOnTicketFound (ContainsTicket (ToT (GetFieldType dt name)))),
KnownValue (GetFieldType dt name))
:- DupableScope (ToT (GetFieldType dt name)))
-> Label name
-> (dt : st) :-> (GetFieldType dt name : dt : st)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((SingI (ToT (GetFieldType dt name)),
FailOnTicketFound (ContainsTicket (ToT (GetFieldType dt name)))),
KnownValue (GetFieldType dt name))
:- DupableScope (ToT (GetFieldType dt name))
forall a. Dupable a :- DupableScope (ToT a)
dupableEvi @(GetFieldType dt name)
where
_needHasDupableGetters :: Dict (HasDupableGetters dt)
_needHasDupableGetters = HasDupableGetters dt => Dict (HasDupableGetters dt)
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 :: 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 :: Label name -> (GetFieldType dt name : dt : st) :-> (dt : st)
setField = Instr
(ToT (GetFieldType dt name) : GValueType (Rep dt) : ToTs st)
(GValueType (Rep dt) : ToTs st)
-> (GetFieldType dt name : dt : st) :-> (dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
(ToT (GetFieldType dt name) : GValueType (Rep dt) : ToTs st)
(GValueType (Rep dt) : ToTs st)
-> (GetFieldType dt name : dt : st) :-> (dt : st))
-> (Label name
-> Instr
(ToT (GetFieldType dt name) : GValueType (Rep dt) : ToTs st)
(GValueType (Rep dt) : ToTs st))
-> Label name
-> (GetFieldType dt name : 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)
forall (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 :: 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 = 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 @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
# Label name -> (GetFieldType dt name : dt : st) :-> (dt : st)
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 :: ('[GetFieldType dt name] :-> '[res, GetFieldType dt name])
-> ('[GetFieldType dt name] :-> '[res])
-> Label name
-> (dt : st) :-> (res : dt : st)
getFieldOpen '[GetFieldType dt name] :-> '[res, GetFieldType dt name]
contWDup '[GetFieldType dt name] :-> '[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
. Instr
'[ToT (GetFieldType dt name)]
'[ToT res, ToT (GetFieldType dt name)]
-> Instr '[ToT (GetFieldType dt name)] '[ToT res]
-> Label name
-> Instr (ToT dt : ToTs st) (ToT res : ToT dt : ToTs st)
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 (('[GetFieldType dt name] :-> '[res, GetFieldType dt name])
-> Instr
(ToTs '[GetFieldType dt name]) (ToTs '[res, GetFieldType dt name])
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iNonFailingCode '[GetFieldType dt name] :-> '[res, GetFieldType dt name]
contWDup) (('[GetFieldType dt name] :-> '[res])
-> Instr (ToTs '[GetFieldType dt name]) (ToTs '[res])
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iNonFailingCode '[GetFieldType dt name] :-> '[res]
contWoDup)
where
_needHasDupableGetters :: Dict (HasDupableGetters dt)
_needHasDupableGetters = HasDupableGetters dt => Dict (HasDupableGetters dt)
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 :: ('[new, GetFieldType dt name] :-> '[GetFieldType dt name])
-> Label name -> (new : dt : st) :-> (dt : st)
setFieldOpen '[new, GetFieldType dt name] :-> '[GetFieldType dt name]
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
. Instr
'[ToT new, ToT (GetFieldType dt name)]
'[ToT (GetFieldType dt name)]
-> Label name
-> Instr (ToT new : ToT dt : ToTs st) (ToT dt : ToTs st)
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, GetFieldType dt name] :-> '[GetFieldType dt name])
-> Instr
(ToTs '[new, GetFieldType dt name]) (ToTs '[GetFieldType dt name])
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iNonFailingCode '[new, GetFieldType dt name] :-> '[GetFieldType dt name]
cont)
construct
:: 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)
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 (st :: [T]).
InstrConstructC dt =>
Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> Instr st (ToT dt : st)
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 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 :: IsoRecTuple fctors -> st :-> (dt : st)
constructT = Rec (FieldConstructor st) (GFieldTypes (Rep dt))
-> st :-> (dt : st)
forall dt (st :: [*]).
(InstrConstructC dt, RMap (ConstructorFieldTypes dt)) =>
Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> st :-> (dt : st)
construct (Rec (FieldConstructor st) (GFieldTypes (Rep dt))
-> st :-> (dt : st))
-> (IsoRecTuple (Rec (FieldConstructor st) (GFieldTypes (Rep dt)))
-> Rec (FieldConstructor st) (GFieldTypes (Rep dt)))
-> IsoRecTuple (Rec (FieldConstructor st) (GFieldTypes (Rep dt)))
-> st :-> (dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsoRecTuple (Rec (FieldConstructor st) (GFieldTypes (Rep dt)))
-> Rec (FieldConstructor st) (GFieldTypes (Rep dt))
forall r. RecFromTuple r => IsoRecTuple r -> r
recFromTuple
constructStack
:: forall dt fields st .
( InstrConstructC dt
, fields ~ ConstructorFieldTypes dt
, KnownList fields
)
=> (fields ++ st) :-> dt : st
constructStack :: (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 (st :: [T]).
(InstrConstructC dt, ToTs fields ~ ToTs (ConstructorFieldTypes dt),
KnownList (ToTs fields)) =>
Instr (ToTs fields ++ st) (ToT dt : st)
forall dt (stack :: [T]) (st :: [T]).
(InstrConstructC dt, stack ~ ToTs (ConstructorFieldTypes dt),
KnownList stack) =>
Instr (stack ++ st) (ToT dt : st)
instrConstructStack @dt @(ToTs fields))
(KnownList (ToTs fields) => (fields ++ st) :-> (dt : st))
-> (KnownList fields :- KnownList (ToTs fields))
-> (fields ++ st) :-> (dt : st)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ KnownList fields :- KnownList (ToTs fields)
forall (s :: [*]). KnownList s :- KnownList (ToTs s)
totsKnownLemma @fields
((ToTs (fields ++ st) ~ (ToTs fields ++ ToTs st)) =>
(fields ++ st) :-> (dt : st))
-> Dict (ToTs (fields ++ st) ~ (ToTs fields ++ ToTs st))
-> (fields ++ st) :-> (dt : st)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ KnownList fields =>
Dict (ToTs (fields ++ st) ~ (ToTs fields ++ ToTs st))
forall (a :: [*]) (b :: [*]).
KnownList a =>
Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
totsAppendLemma @fields @st
deconstruct
:: forall dt fields st .
( InstrDeconstructC dt
, KnownList fields
, fields ~ ConstructorFieldTypes dt
)
=> dt : st :-> (fields ++ st)
deconstruct :: (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 (st :: [T]).
(InstrDeconstructC dt,
ToTs fields ~ ToTs (ConstructorFieldTypes dt),
KnownList (ToTs fields)) =>
Instr (ToT dt : st) (ToTs fields ++ st)
forall dt (stack :: [T]) (st :: [T]).
(InstrDeconstructC dt, stack ~ ToTs (ConstructorFieldTypes dt),
KnownList stack) =>
Instr (ToT dt : st) (stack ++ st)
instrDeconstruct @dt @(ToTs fields))
(KnownList (ToTs fields) => (dt : st) :-> (fields ++ st))
-> (KnownList fields :- KnownList (ToTs fields))
-> (dt : st) :-> (fields ++ st)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ KnownList fields :- KnownList (ToTs fields)
forall (s :: [*]). KnownList s :- KnownList (ToTs s)
totsKnownLemma @fields
((ToTs (fields ++ st) ~ (ToTs fields ++ ToTs st)) =>
(dt : st) :-> (fields ++ st))
-> Dict (ToTs (fields ++ st) ~ (ToTs fields ++ ToTs st))
-> (dt : st) :-> (fields ++ st)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ KnownList fields =>
Dict (ToTs (fields ++ st) ~ (ToTs fields ++ ToTs st))
forall (a :: [*]) (b :: [*]).
KnownList a =>
Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
totsAppendLemma @fields @st
fieldCtor :: HasCallStack => (st :-> f : st) -> FieldConstructor st f
fieldCtor :: (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_ :: Label name
-> AppendCtorField (GetCtorField dt name) st :-> (dt : st)
wrap_ =
case (AppendCtorFieldAxiom ('OneField Word) '[Int],
AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom (GetCtorField dt name) st)
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
(ToTs (AppendCtorField (GetCtorField dt name) st))
(GValueType (Rep dt) : ToTs st)
-> AppendCtorField (GetCtorField dt name) st :-> (dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
(ToTs (AppendCtorField (GetCtorField dt name) st))
(GValueType (Rep dt) : ToTs st)
-> AppendCtorField (GetCtorField dt name) st :-> (dt : st))
-> (Label name
-> Instr
(ToTs (AppendCtorField (GetCtorField dt name) st))
(GValueType (Rep dt) : ToTs st))
-> Label name
-> AppendCtorField (GetCtorField dt name) 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)
forall (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 :: Label name -> (CtorOnlyField name dt : st) :-> (dt : st)
wrapOne = case (AppendCtorFieldAxiom ('OneField Word) '[Int],
AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom (GetCtorField dt name) st)
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)
forall (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_ :: 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 (out :: [T]) (inp :: [T]).
InstrCaseC dt =>
Rec (CaseClause inp out) (CaseClauses dt)
-> RemFail Instr (ToT dt : inp) out
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 :: CaseClauseL inp out clauses
-> CaseClause (ToTs inp) (ToTs out) clauses
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 Proxy clauses
forall k (t :: k). Proxy t
Proxy @clauses of
(_ :: Proxy ('CaseClauseParam ctor cc)) ->
case (AppendCtorFieldAxiom ('OneField Word) '[Int],
AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom x inp)
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 :: IsoRecTuple clauses -> (dt : inp) :-> out
caseT = forall (out :: [*]) (inp :: [*]).
(InstrCaseC dt, RMap (GCaseClauses (Rep dt))) =>
Rec (CaseClauseL inp out) (GCaseClauses (Rep dt))
-> (dt : inp) :-> out
forall dt (out :: [*]) (inp :: [*]).
(InstrCaseC dt, RMap (CaseClauses dt)) =>
Rec (CaseClauseL inp out) (CaseClauses dt) -> (dt : inp) :-> out
case_ @dt (Rec (CaseClauseL inp out) (GCaseClauses (Rep dt))
-> (dt : inp) :-> out)
-> (IsoRecTuple (Rec (CaseClauseL inp out) (GCaseClauses (Rep dt)))
-> Rec (CaseClauseL inp out) (GCaseClauses (Rep dt)))
-> IsoRecTuple (Rec (CaseClauseL inp out) (GCaseClauses (Rep dt)))
-> (dt : inp) :-> out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsoRecTuple (Rec (CaseClauseL inp out) (GCaseClauses (Rep dt)))
-> Rec (CaseClauseL inp out) (GCaseClauses (Rep 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_ :: Label name -> (dt : st) :-> (CtorOnlyField name dt : st)
unsafeUnwrap_ =
case (AppendCtorFieldAxiom ('OneField Word) '[Int],
AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom (GetCtorField dt name) st)
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
(GValueType (Rep dt) : ToTs st)
(ToT (CtorOnlyField name dt) : ToTs st)
-> (dt : st) :-> (CtorOnlyField name dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
(GValueType (Rep dt) : ToTs st)
(ToT (CtorOnlyField name dt) : ToTs st)
-> (dt : st) :-> (CtorOnlyField name dt : st))
-> (Label name
-> Instr
(GValueType (Rep dt) : ToTs st)
(ToT (CtorOnlyField name dt) : ToTs st))
-> Label name
-> (dt : st) :-> (CtorOnlyField name 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)
forall (name :: Symbol) (st :: [T]).
InstrUnwrapC dt name =>
Label name
-> Instr (ToT dt : st) (ToT (CtorOnlyField name dt) : st)
unsafeInstrUnwrap @dt