{-# LANGUAGE FunctionalDependencies #-}
module Lorentz.ADT
( HasField
, HasFieldOfType
, HasFieldsOfType
, NamedField (..)
, (:=)
, toField
, toFieldNamed
, getField
, getFieldNamed
, setField
, modifyField
, construct
, constructT
, fieldCtor
, wrap_
, case_
, caseT
, unwrapUnsafe_
, CaseTC
, CaseArrow (..)
, CaseClauseL (..)
, InstrConstructC
, ConstructorFieldTypes
, Rec (..)
, (:!)
, (:?)
, arg
, argDef
, argF
) where
import Data.Constraint (Dict(..))
import qualified Data.Kind as Kind
import Data.Vinyl.Core (RMap(..), Rec(..))
import Data.Vinyl.Derived (Label)
import GHC.TypeLits (AppendSymbol, Symbol)
import Named ((:!), (:?), arg, argDef, argF)
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Instr
import Michelson.Typed.Haskell.Instr
import Michelson.Typed.Haskell.Value
import 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 Kind.Type
type n := ty = 'NamedField n ty
infixr 0 :=
type family HasFieldsOfType (dt :: Kind.Type) (fs :: [NamedField])
:: Constraint where
HasFieldsOfType _ '[] = ()
HasFieldsOfType dt ((n := ty) ': fs) =
(HasFieldOfType dt n ty, HasFieldsOfType dt fs)
toField
:: forall dt name st.
InstrGetFieldC dt name
=> Label name -> dt & st :-> GetFieldType dt name & st
toField = I . instrGetField @dt
toFieldNamed
:: forall dt name st.
InstrGetFieldC dt name
=> Label name -> dt & st :-> (name :! GetFieldType dt name) & st
toFieldNamed l = toField l # forcedCoerce_
getField
:: forall dt name st.
InstrGetFieldC dt name
=> Label name -> dt & st :-> GetFieldType dt name & dt ': st
getField l = dup # toField @dt l
getFieldNamed
:: forall dt name st.
InstrGetFieldC dt name
=> Label name -> dt & st :-> (name :! GetFieldType dt name) & dt ': st
getFieldNamed l = getField l # coerceWrap
setField
:: forall dt name st.
InstrSetFieldC dt name
=> Label name -> (GetFieldType dt name ': dt ': st) :-> (dt ': st)
setField = I . instrSetField @dt
modifyField
:: forall dt name st.
( InstrGetFieldC dt name
, InstrSetFieldC dt name
)
=> Label name
-> (forall st0. (GetFieldType dt name ': st0) :-> (GetFieldType dt name ': st0))
-> dt & st :-> dt & st
modifyField l i = getField @dt l # i # setField @dt l
construct
:: forall dt st.
( InstrConstructC dt
, RMap (ConstructorFieldTypes dt)
)
=> Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> st :-> dt & st
construct fctors =
I $ instrConstruct @dt $
rmap (\(FieldConstructor i) -> FieldConstructor i) 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 = construct . recFromTuple
fieldCtor :: HasCallStack => (st :-> f & st) -> FieldConstructor st f
fieldCtor = \case
I i -> FieldConstructor i
FI _ -> error "Field constructor always fails"
wrap_
:: forall dt name st.
InstrWrapC dt name
=> Label name -> (AppendCtorField (GetCtorField dt name) st) :-> dt & st
wrap_ =
case appendCtorFieldAxiom @(GetCtorField dt name) @st of
Dict -> I . instrWrap @dt
data CaseClauseL (inp :: [Kind.Type]) (out :: [Kind.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
(/->) _ = CaseClauseL
case_
:: forall dt out inp.
( InstrCaseC dt inp out
, RMap (CaseClauses dt)
)
=> Rec (CaseClauseL inp out) (CaseClauses dt) -> dt & inp :-> out
case_ = LorentzInstr . instrCase @dt . rmap coerceCaseClause
where
coerceCaseClause
:: forall clauses.
CaseClauseL inp out clauses -> CaseClause (ToTs inp) (ToTs out) clauses
coerceCaseClause (CaseClauseL (LorentzInstr cc)) =
CaseClause $ case Proxy @clauses of
(_ :: Proxy ('CaseClauseParam ctor cc)) ->
case appendCtorFieldAxiom @cc @inp of Dict -> cc
caseT
:: forall dt out inp clauses.
CaseTC dt out inp clauses
=> IsoRecTuple clauses -> dt & inp :-> out
caseT = case_ @dt . recFromTuple
type CaseTC dt out inp clauses =
( InstrCaseC dt inp out
, RMap (CaseClauses dt)
, RecFromTuple clauses
, clauses ~ Rec (CaseClauseL inp out) (CaseClauses dt)
)
unwrapUnsafe_
:: forall dt name st.
InstrUnwrapC dt name
=> Label name -> dt & st :-> (CtorOnlyField name dt ': st)
unwrapUnsafe_ =
case appendCtorFieldAxiom @(GetCtorField dt name) @st of
Dict -> I . instrUnwrapUnsafe @dt