{-# LANGUAGE DeriveAnyClass, DerivingStrategies #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Michelson.Typed.Haskell.Instr.Sum
( InstrWrapC
, InstrCaseC
, InstrUnwrapC
, instrWrap
, hsWrap
, instrCase
, (//->)
, instrUnwrapUnsafe
, hsUnwrap
, CaseClauseParam (..)
, CaseClause (..)
, CaseClauses
, CtorField (..)
, ExtractCtorField
, AppendCtorField
, AppendCtorFieldAxiom
, appendCtorFieldAxiom
, GetCtorField
, CtorHasOnlyField
, CtorOnlyField
, MyCompoundType
) where
import Data.Constraint (Dict(..))
import qualified Data.Kind as Kind
import Data.Singletons (SingI(..))
import Data.Type.Bool (If, type (||))
import Data.Type.Equality (type (==))
import Data.Vinyl.Core (Rec(..))
import Data.Vinyl.Derived (Label)
import Data.Vinyl.TypeLevel (type (++))
import GHC.Generics ((:*:)(..), (:+:)(..))
import qualified GHC.Generics as G
import GHC.TypeLits (AppendSymbol, ErrorMessage(..), Symbol, TypeError)
import Named ((:!))
import Type.Reflection ((:~:)(Refl))
import Unsafe.Coerce (unsafeCoerce)
import Michelson.Typed.Haskell.Instr.Helpers
import Michelson.Typed.Haskell.Value
import Michelson.Typed.Instr
import Michelson.Typed.T
import Michelson.Text (mt)
import Michelson.Typed.Value
import Tezos.Address (Address)
import Tezos.Core (Mutez, Timestamp)
import Tezos.Crypto (KeyHash, PublicKey, Signature)
import Util.TypeTuple
data CtorField
= OneField Kind.Type
| NoFields
type family ExtractCtorField (cf :: CtorField) where
ExtractCtorField ('OneField t) = t
ExtractCtorField 'NoFields = ()
type family AppendCtorField (cf :: CtorField) (l :: [k]) :: [k] where
AppendCtorField ('OneField t) (l :: [T]) = ToT t ': l
AppendCtorField ('OneField t) (l :: [Kind.Type]) = t ': l
AppendCtorField 'NoFields (l :: [T]) = l
AppendCtorField 'NoFields (l :: [Kind.Type]) = l
type AppendCtorFieldAxiom (cf :: CtorField) (st :: [Kind.Type]) =
ToTs (AppendCtorField cf st) ~ AppendCtorField cf (ToTs st)
appendCtorFieldAxiom
:: ( AppendCtorFieldAxiom ('OneField Word) '[Int]
, AppendCtorFieldAxiom 'NoFields '[Int]
)
=> Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom =
unsafeCoerce $ 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 (G.Rep a))
type family LNRequireFound
(name :: Symbol)
(a :: Kind.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 :: Kind.Type -> Kind.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 :: Kind.Type -> Kind.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 CanGoDeeper (x :: Kind.Type) :: Bool where
CanGoDeeper Integer = 'False
CanGoDeeper Natural = 'False
CanGoDeeper Text = 'False
CanGoDeeper Bool = 'False
CanGoDeeper ByteString = 'False
CanGoDeeper Mutez = 'False
CanGoDeeper Address = 'False
CanGoDeeper KeyHash = 'False
CanGoDeeper Timestamp = 'False
CanGoDeeper PublicKey = 'False
CanGoDeeper Signature = 'False
CanGoDeeper (ContractAddr _) = 'False
CanGoDeeper (BigMap _ _) = 'False
CanGoDeeper (Map _ _) = 'False
CanGoDeeper (Set _) = 'False
CanGoDeeper ([_]) = 'False
CanGoDeeper x = GCanGoDeeper (G.Rep x)
type family GLookupNamedDeeper (name :: Symbol) (x :: Kind.Type -> Kind.Type)
:: Maybe LookupNamedResult where
GLookupNamedDeeper name (G.S1 _ (G.Rec0 y)) = GLookupNamed name (G.Rep 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 GExtractFields (x :: Kind.Type -> Kind.Type)
:: CtorField where
GExtractFields (G.S1 _ x) = GExtractFields x
GExtractFields (G.Rec0 a) = 'OneField a
GExtractFields G.U1 = 'NoFields
GExtractFields (_ :*: _) = 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) :: Kind.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 _ =
gInstrWrap @(G.Rep dt) @(LnrBranch (GetNamed name dt))
@(LnrFieldType (GetNamed name dt))
type InstrWrapC dt name =
( IsoValue dt, Generic dt
, GInstrWrap (G.Rep dt)
(LnrBranch (GetNamed name dt))
(LnrFieldType (GetNamed name dt))
, GValueType (G.Rep dt) ~ ToT dt
)
hsWrap
:: forall dt name.
InstrWrapC dt name
=> Label name
-> ExtractCtorField (GetCtorField dt name)
-> dt
hsWrap _ =
G.to . gHsWrap @(G.Rep dt) @(LnrBranch (GetNamed name dt))
@(LnrFieldType (GetNamed name dt))
class GIsoValue x =>
GInstrWrap
(x :: Kind.Type -> Kind.Type)
(path :: Path)
(entryTy :: CtorField) where
gInstrWrap
:: GIsoValue x
=> Instr (AppendCtorField entryTy s) (GValueType x ': s)
gHsWrap
:: GIsoValue x
=> ExtractCtorField entryTy -> x p
instance GInstrWrap x path e => GInstrWrap (G.D1 i x) path e where
gInstrWrap = gInstrWrap @x @path @e
gHsWrap = G.M1 . gHsWrap @x @path @e
instance (GInstrWrap x path e, GIsoValue y, SingI (GValueType y)) =>
GInstrWrap (x :+: y) ('L ': path) e where
gInstrWrap = gInstrWrap @x @path @e `Seq` LEFT
gHsWrap = G.L1 . gHsWrap @x @path @e
instance (GInstrWrap y path e, GIsoValue x, SingI (GValueType x)) =>
GInstrWrap (x :+: y) ('R ': path) e where
gInstrWrap = gInstrWrap @y @path @e `Seq` RIGHT
gHsWrap = G.R1 . gHsWrap @y @path @e
instance (IsoValue e) =>
GInstrWrap (G.C1 c (G.S1 i (G.Rec0 e))) '[ 'S] ('OneField e) where
gInstrWrap = Nop
gHsWrap = G.M1 . G.M1 . G.K1
instance ( path ~ (x ': xs)
, GInstrWrap (G.Rep sub) path e
, Generic sub
, GIsoValue (G.Rep sub), IsoValue sub, GValueType (G.Rep sub) ~ ToT sub
) =>
GInstrWrap (G.C1 c (G.S1 i (G.Rec0 sub))) ('S ': x ': xs) e where
gInstrWrap = gInstrWrap @(G.Rep sub) @path @e
gHsWrap = G.M1 . G.M1 . G.K1 . G.to . gHsWrap @(G.Rep sub) @path @e
instance GInstrWrap (G.C1 c G.U1) '[ 'S] 'NoFields where
gInstrWrap = PUSH VUnit
gHsWrap () = G.M1 G.U1
data MyType
= MyCtor Integer
| ComplexThing ()
| UselessThing ("field1" :! ByteString, "field2" :! ())
deriving stock Generic
deriving anyclass IsoValue
_MyTypeMyCtor ::
GetNamed "cMyCtor" MyType :~: 'LNR ('OneField Integer) '[ 'L, 'S]
_MyTypeMyCtor = Refl
_MyTypeComplexThing ::
GetNamed "cComplexThing" MyType :~: 'LNR ('OneField ()) '[ 'R, 'L, 'S]
_MyTypeComplexThing = Refl
_wrapMyType1 :: Instr (ToT Integer ': s) (ToT MyType ': s)
_wrapMyType1 = instrWrap @MyType #cMyCtor
_wrapMyType1' :: Instr (ToT Integer ': s) (ToT MyType ': s)
_wrapMyType1' = instrWrap @MyType @"MyCtor" fromLabel
_wrapMyType2 :: Instr (ToT () ': s) (ToT MyType ': s)
_wrapMyType2 = instrWrap @MyType #cComplexThing
_wrapMyType3 :: Instr (ToT (ByteString, ()) ': s) (ToT MyType ': s)
_wrapMyType3 = instrWrap @MyType #cUselessThing
data MyType' = WrapBool Bool
deriving stock Generic
deriving anyclass IsoValue
_MyType'WrapBool ::
GetNamed "cWrapBool" MyType' :~: 'LNR ('OneField Bool) '[ 'S]
_MyType'WrapBool = Refl
_wrapMyType' :: Instr (ToT Bool ': s) (ToT MyType' ': s)
_wrapMyType' = instrWrap @MyType' #cWrapBool
data MyCompoundType
= CompoundPart1 MyType
| CompoundPart2 Integer
| CompoundPart3 Address
| CompoundPart4 MyType'
deriving stock Generic
deriving anyclass IsoValue
_MyCompoundTypeCompoundPart1 ::
GetNamed "cCompoundPart1" MyCompoundType :~: 'LNR ('OneField MyType) '[ 'L, 'L, 'S]
_MyCompoundTypeCompoundPart1 = Refl
_MyCompoundTypeMyCtor ::
GetNamed "cMyCtor" MyCompoundType :~: 'LNR ('OneField Integer) '[ 'L, 'L, 'S, 'L, 'S]
_MyCompoundTypeMyCtor = Refl
_MyCompoundTypeCompoundPart2 ::
GetNamed "cCompoundPart2" MyCompoundType :~: 'LNR ('OneField Integer) '[ 'L, 'R, 'S]
_MyCompoundTypeCompoundPart2 = Refl
_MyCompoundTypeCompoundPart4 ::
GetNamed "cCompoundPart4" MyCompoundType :~: 'LNR ('OneField MyType') '[ 'R, 'R, 'S]
_MyCompoundTypeCompoundPart4 = Refl
_MyCompoundTypeWrapBool ::
GetNamed "cWrapBool" MyCompoundType :~: 'LNR ('OneField Bool) '[ 'R, 'R, 'S, 'S]
_MyCompoundTypeWrapBool = Refl
_wrapMyCompoundType1 :: Instr (ToT Integer ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType1 = instrWrap @MyCompoundType #cMyCtor
_wrapMyCompoundType2 :: Instr (ToT Integer ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType2 = instrWrap @MyCompoundType #cCompoundPart2
_wrapMyCompoundType3 :: Instr (ToT Bool ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType3 = instrWrap @MyCompoundType #cWrapBool
_wrapMyCompoundType4 :: Instr (ToT MyType' ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType4 = instrWrap @MyCompoundType #cCompoundPart4
data MyEnum = Case1 | Case2 | CaseN Integer | CaseDef
deriving stock Generic
deriving anyclass IsoValue
_wrapMyEnum1 :: Instr s (ToT MyEnum ': s)
_wrapMyEnum1 = instrWrap @MyEnum #cCase1
_wrapMyEnum2 :: Instr (ToT Integer ': s) (ToT MyEnum ': s)
_wrapMyEnum2 = instrWrap @MyEnum #cCaseN
instrCase
:: forall dt out inp.
InstrCaseC dt inp out
=> Rec (CaseClause inp out) (CaseClauses dt) -> Instr (ToT dt ': inp) out
instrCase = gInstrCase @(G.Rep dt)
type InstrCaseC dt inp out =
( IsoValue dt
, GInstrCase (G.Rep dt)
, GValueType (G.Rep dt) ~ ToT dt
)
data CaseClauseParam = CaseClauseParam Symbol CtorField
data CaseClause (inp :: [T]) (out :: [T]) (param :: CaseClauseParam) where
CaseClause :: Instr (AppendCtorField x inp) out -> CaseClause inp out ('CaseClauseParam ctor x)
(//->)
:: Label ("c" `AppendSymbol` ctor)
-> Instr (AppendCtorField x inp) out
-> CaseClause inp out ('CaseClauseParam ctor x)
(//->) _ = CaseClause
infixr 8 //->
type CaseClauses a = GCaseClauses (G.Rep a)
class GIsoValue x => GInstrCase (x :: Kind.Type -> Kind.Type) where
type GCaseClauses x :: [CaseClauseParam]
gInstrCase
:: GIsoValue x
=> Rec (CaseClause inp out) (GCaseClauses x) -> Instr (GValueType x ': inp) out
instance GInstrCase x => GInstrCase (G.D1 i x) where
type GCaseClauses (G.D1 i x) = GCaseClauses x
gInstrCase = gInstrCase @x
instance (GInstrCase x, GInstrCase y, RSplit (GCaseClauses x) (GCaseClauses y)) =>
GInstrCase (x :+: y) where
type GCaseClauses (x :+: y) = GCaseClauses x ++ GCaseClauses y
gInstrCase clauses =
let (leftClauses, rightClauses) = rsplit clauses
lbranch = gInstrCase @x leftClauses
rbranch = gInstrCase @y rightClauses
in IF_LEFT lbranch rbranch
instance GInstrCaseBranch ctor x => GInstrCase (G.C1 ('G.MetaCons ctor _1 _2) x) where
type GCaseClauses (G.C1 ('G.MetaCons ctor _1 _2) x) = '[GCaseBranchInput ctor x]
gInstrCase (clause :& RNil) = gInstrCaseBranch @ctor @x clause
class GIsoValue x =>
GInstrCaseBranch (ctor :: Symbol) (x :: Kind.Type -> Kind.Type) where
type GCaseBranchInput ctor x :: CaseClauseParam
gInstrCaseBranch
:: CaseClause inp out (GCaseBranchInput ctor x)
-> Instr (GValueType x ': inp) out
instance
( GIsoValue x, GIsoValue y
, TypeError ('Text "Cannot pattern match on constructors with more than 1 field"
':$$: 'Text "Consider using tuples instead")
) => GInstrCaseBranch ctor (x :*: y) where
type GCaseBranchInput ctor (x :*: y) = 'CaseClauseParam ctor 'NoFields
gInstrCaseBranch = error "impossible"
instance GInstrCaseBranch ctor x => GInstrCaseBranch ctor (G.S1 i x) where
type GCaseBranchInput ctor (G.S1 i x) = GCaseBranchInput ctor x
gInstrCaseBranch = gInstrCaseBranch @ctor @x
instance IsoValue a => GInstrCaseBranch ctor (G.Rec0 a) where
type GCaseBranchInput ctor (G.Rec0 a) = 'CaseClauseParam ctor ('OneField a)
gInstrCaseBranch (CaseClause i) = i
instance GInstrCaseBranch ctor G.U1 where
type GCaseBranchInput ctor G.U1 = 'CaseClauseParam ctor 'NoFields
gInstrCaseBranch (CaseClause i) = DROP `Seq` i
_caseMyType :: Instr (ToT MyType ': s) (ToT Integer ': s)
_caseMyType = instrCase @MyType $
#cMyCtor //-> Nop
:& #cComplexThing //-> (DROP `Seq` PUSH (toVal @Integer 5))
:& #cUselessThing //-> (DROP `Seq` PUSH (toVal @Integer 0))
:& RNil
_caseMyType2 :: Instr (ToT MyType ': s) (ToT Integer ': s)
_caseMyType2 = instrCase @MyType $ recFromTuple
( #cMyCtor //->
Nop
, #cComplexThing //->
(DROP `Seq` PUSH (toVal @Integer 5))
, #cUselessThing //->
(DROP `Seq` PUSH (toVal @Integer 0))
)
_caseMyEnum :: Instr (ToT MyEnum ': ToT Integer ': s) (ToT Integer ': s)
_caseMyEnum = instrCase @MyEnum $ recFromTuple
( #cCase1 //-> (DROP `Seq` PUSH (toVal @Integer 1))
, #cCase2 //-> (DROP `Seq` PUSH (toVal @Integer 2))
, #cCaseN //-> (DIP DROP `Seq` Nop)
, #cCaseDef //-> Nop
)
instrUnwrapUnsafe
:: forall dt name st.
InstrUnwrapC dt name
=> Label name
-> Instr (ToT dt ': st)
(ToT (CtorOnlyField name dt) ': st)
instrUnwrapUnsafe _ =
gInstrUnwrapUnsafe @(G.Rep dt) @(LnrBranch (GetNamed name dt))
@(CtorOnlyField name dt)
type InstrUnwrapC dt name =
( IsoValue dt, Generic dt
, GInstrUnwrap (G.Rep dt)
(LnrBranch (GetNamed name dt))
(CtorOnlyField name dt)
, GValueType (G.Rep dt) ~ ToT dt
)
hsUnwrap
:: forall dt name.
InstrUnwrapC dt name
=> Label name
-> dt
-> Maybe (CtorOnlyField name dt)
hsUnwrap _ =
gHsUnwrap @(G.Rep dt) @(LnrBranch (GetNamed name dt))
@(CtorOnlyField name dt) .
G.from
class GIsoValue x =>
GInstrUnwrap
(x :: Kind.Type -> Kind.Type)
(path :: Path)
(entryTy :: Kind.Type) where
gInstrUnwrapUnsafe
:: GIsoValue x
=> 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
gInstrUnwrapUnsafe = gInstrUnwrapUnsafe @x @path @e
gHsUnwrap = gHsUnwrap @x @path @e . G.unM1
instance (GInstrUnwrap x path e, GIsoValue y, SingI (GValueType y)) =>
GInstrUnwrap (x :+: y) ('L ': path) e where
gInstrUnwrapUnsafe = IF_LEFT (gInstrUnwrapUnsafe @x @path @e) failWithWrongCtor
gHsUnwrap = \case
G.L1 x -> gHsUnwrap @x @path @e x
G.R1 _ -> Nothing
instance (GInstrUnwrap y path e, GIsoValue x, SingI (GValueType x)) =>
GInstrUnwrap (x :+: y) ('R ': path) e where
gInstrUnwrapUnsafe = IF_LEFT failWithWrongCtor (gInstrUnwrapUnsafe @y @path @e)
gHsUnwrap = \case
G.R1 y -> gHsUnwrap @y @path @e y
G.L1 _ -> Nothing
instance (IsoValue e) =>
GInstrUnwrap (G.C1 c (G.S1 i (G.Rec0 e))) '[ 'S] e where
gInstrUnwrapUnsafe = Nop
gHsUnwrap = Just . G.unK1 . G.unM1 . G.unM1
instance ( path ~ (x ': xs)
, GInstrUnwrap (G.Rep sub) path e
, Generic sub
, GIsoValue (G.Rep sub), IsoValue sub, GValueType (G.Rep sub) ~ ToT sub
) =>
GInstrUnwrap (G.C1 c (G.S1 i (G.Rec0 sub))) ('S ': x ': xs) e where
gInstrUnwrapUnsafe = gInstrUnwrapUnsafe @(G.Rep sub) @path @e
gHsUnwrap = gHsUnwrap @(G.Rep sub) @path @e . G.from . G.unK1 . G.unM1 . G.unM1
failWithWrongCtor :: Instr i o
failWithWrongCtor =
PUSH (toVal [mt|unwrapUnsafe: unexpected constructor|]) `Seq`
FAILWITH
_unwrapMyType :: Instr (ToT MyType ': s) (ToT Integer ': s)
_unwrapMyType = instrUnwrapUnsafe @MyType #cMyCtor
_unwrapMyCompoundType :: Instr (ToT MyCompoundType ': s) (ToT Integer ': s)
_unwrapMyCompoundType = instrUnwrapUnsafe @MyCompoundType #cMyCtor
_unwrapMyCompoundType2 :: Instr (ToT MyCompoundType ': s) (ToT Address ': s)
_unwrapMyCompoundType2 = instrUnwrapUnsafe @MyCompoundType #cCompoundPart3
_unwrapMyCompoundType3 :: Instr (ToT MyCompoundType ': s) (ToT Bool ': s)
_unwrapMyCompoundType3 = instrUnwrapUnsafe @MyCompoundType #cWrapBool
_unwrapMyCompoundType4 :: Instr (ToT MyCompoundType ': s) (ToT MyType' ': s)
_unwrapMyCompoundType4 = instrUnwrapUnsafe @MyCompoundType #cCompoundPart4