{-# LANGUAGE DataKinds, GADTs #-}
module Michelson.Typed.Annotation
( Notes (..)
, AnnConvergeError(..)
, converge
, convergeAnns
, orAnn
, isStar
, starNotes
) where
import Data.Default (Default(..))
import qualified Data.Kind as Kind
import Data.Singletons (SingI(..))
import Fmt (Buildable(..), (+|), (|+))
import Michelson.Typed.T (T(..))
import Michelson.Typed.Sing
import Michelson.Untyped.Annotation (Annotation, FieldAnn, TypeAnn, unifyAnn, noAnn)
import Util.Typeable
data Notes t where
NTc :: TypeAnn -> Notes ('Tc ct)
NTKey :: TypeAnn -> Notes 'TKey
NTUnit :: TypeAnn -> Notes 'TUnit
NTSignature :: TypeAnn -> Notes 'TSignature
NTChainId :: TypeAnn -> Notes 'TChainId
NTOption :: TypeAnn -> Notes t -> Notes ('TOption t)
NTList :: TypeAnn -> Notes t -> Notes ('TList t)
NTSet :: TypeAnn -> TypeAnn -> Notes ('TSet ct)
NTOperation :: TypeAnn -> Notes 'TOperation
NTContract :: TypeAnn -> Notes t -> Notes ('TContract t)
NTPair :: TypeAnn -> FieldAnn -> FieldAnn
-> Notes p -> Notes q -> Notes ('TPair p q)
NTOr :: TypeAnn -> FieldAnn -> FieldAnn
-> Notes p -> Notes q -> Notes ('TOr p q)
NTLambda :: TypeAnn -> Notes p -> Notes q -> Notes ('TLambda p q)
NTMap :: TypeAnn -> TypeAnn -> Notes v -> Notes ('TMap k v)
NTBigMap :: TypeAnn -> TypeAnn -> Notes v -> Notes ('TBigMap k v)
deriving stock instance Show (Notes t)
deriving stock instance Eq (Notes t)
starNotes :: forall t. SingI t => Notes t
starNotes = case sing @t of
STc _ -> NTc noAnn
STKey -> NTKey noAnn
STUnit -> NTUnit noAnn
STSignature -> NTSignature noAnn
STChainId -> NTChainId noAnn
STOperation -> NTOperation noAnn
STSet _ -> NTSet noAnn noAnn
STList _ -> NTList noAnn starNotes
STOption _ -> NTOption noAnn starNotes
STContract _ -> NTContract noAnn starNotes
STMap _ _ -> NTMap noAnn noAnn starNotes
STBigMap _ _ -> NTBigMap noAnn noAnn starNotes
STPair _ _ -> NTPair noAnn noAnn noAnn starNotes starNotes
STOr _ _ -> NTOr noAnn noAnn noAnn starNotes starNotes
STLambda _ _ -> NTLambda noAnn starNotes starNotes
isStar :: SingI t => Notes t -> Bool
isStar = (== starNotes)
orAnn :: Annotation t -> Annotation t -> Annotation t
orAnn a b = bool a b (a == def)
converge :: Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge (NTc a) (NTc b) = NTc <$> convergeAnns a b
converge (NTKey a) (NTKey b) = NTKey <$> convergeAnns a b
converge (NTUnit a) (NTUnit b) = NTUnit <$> convergeAnns a b
converge (NTSignature a) (NTSignature b) =
NTSignature <$> convergeAnns a b
converge (NTChainId a) (NTChainId b) =
NTChainId <$> convergeAnns a b
converge (NTOption a n) (NTOption b m) =
NTOption <$> convergeAnns a b <*> converge n m
converge (NTList a n) (NTList b m) =
NTList <$> convergeAnns a b <*> converge n m
converge (NTSet a n) (NTSet b m) =
NTSet <$> convergeAnns a b <*> convergeAnns n m
converge (NTOperation a) (NTOperation b) =
NTOperation <$> convergeAnns a b
converge (NTContract a n) (NTContract b m) =
NTContract <$> convergeAnns a b <*> converge n m
converge (NTPair a pF qF pN qN) (NTPair b pG qG pM qM) =
NTPair <$> convergeAnns a b <*> convergeAnns pF pG
<*> convergeAnns qF qG <*> converge pN pM <*> converge qN qM
converge (NTOr a pF qF pN qN) (NTOr b pG qG pM qM) =
NTOr <$> convergeAnns a b <*> convergeAnns pF pG <*> convergeAnns qF qG
<*> converge pN pM <*> converge qN qM
converge (NTLambda a pN qN) (NTLambda b pM qM) =
NTLambda <$> convergeAnns a b <*> converge pN pM <*> converge qN qM
converge (NTMap a kN vN) (NTMap b kM vM) =
NTMap <$> convergeAnns a b <*> convergeAnns kN kM <*> converge vN vM
converge (NTBigMap a kN vN) (NTBigMap b kM vM) =
NTBigMap <$> convergeAnns a b <*> convergeAnns kN kM <*> converge vN vM
data AnnConvergeError where
AnnConvergeError
:: forall (tag :: Kind.Type).
(Buildable (Annotation tag), Show (Annotation tag), Typeable tag)
=> Annotation tag -> Annotation tag -> AnnConvergeError
deriving stock instance Show AnnConvergeError
instance Eq AnnConvergeError where
AnnConvergeError ann1 ann2 == AnnConvergeError ann1' ann2' =
(ann1 `eqParam1` ann1') && (ann2 `eqParam1` ann2')
instance Buildable AnnConvergeError where
build (AnnConvergeError ann1 ann2) =
"Annotations do not converge: " +| ann1 |+ " /= " +| ann2 |+ ""
convergeAnns
:: forall (tag :: Kind.Type).
(Buildable (Annotation tag), Show (Annotation tag), Typeable tag)
=> Annotation tag -> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns a b = maybe (Left $ AnnConvergeError a b)
pure $ unifyAnn a b