{-# 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 :: 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
(DupableScope (ToT (GetFieldType dt name)) =>
Label name -> (dt : st) :-> (GetFieldType dt name : dt : st))
-> (Dupable (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
\\ forall a. Dupable a :- DupableScope (ToT a)
dupableEvi @(GetFieldType dt name)
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
, KnownList fields
)
=> (fields ++ st) :-> dt : st
constructStack :: forall dt (fields :: [*]) (st :: [*]).
(InstrConstructC dt, fields ~ ConstructorFieldTypes dt,
KnownList fields) =>
(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),
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
\\ 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
\\ 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 :: forall dt (fields :: [*]) (st :: [*]).
(InstrDeconstructC dt, KnownList fields,
fields ~ ConstructorFieldTypes dt) =>
(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, 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
\\ 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
\\ 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 :: 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