{-# LANGUAGE DataKinds, GADTs #-}
module Michelson.Typed.Annotation
( Notes (..)
, Notes' (..)
, AnnConvergeError(..)
, converge
, convergeAnns
, notesCase
, isStar
, mkNotes
, orAnn
) where
import Data.Default (Default(..))
import qualified Data.Kind as Kind
import Fmt (Buildable(..), (+|), (|+))
import Michelson.EqParam
import Michelson.Typed.T (T(..))
import Michelson.Untyped.Annotation (Annotation, FieldAnn, TypeAnn, unifyAnn)
data Notes t = N (Notes' t) | NStar
deriving (Eq)
deriving instance Show (Notes p)
notesCase :: r -> (Notes' t -> r) -> Notes t -> r
notesCase a _ NStar = a
notesCase _ f (N b) = f b
data Notes' t where
NTc :: TypeAnn -> Notes' ('Tc ct)
NTKey :: TypeAnn -> Notes' 'TKey
NTUnit :: TypeAnn -> Notes' 'TUnit
NTSignature :: TypeAnn -> Notes' 'TSignature
NTOption :: TypeAnn -> FieldAnn -> 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 instance Show (Notes' t)
deriving instance Eq (Notes' t)
isStar :: Notes t -> Bool
isStar NStar = True
isStar _ = False
isDef :: (Eq t, Default t) => t -> Bool
isDef = (== def)
mkNotes :: Notes' t -> Notes t
mkNotes (NTOption tn fn ns) | isStar ns && isDef tn && isDef fn = NStar
mkNotes (NTList tn ns) | isStar ns && isDef tn = NStar
mkNotes (NTSet tn en) | isDef tn && isDef en = NStar
mkNotes (NTContract tn ns) | isStar ns && isDef tn = NStar
mkNotes (NTPair tn fn1 fn2 ns1 ns2)
| isStar ns1 && isStar ns2 && isDef tn && isDef fn1 && isDef fn2 = NStar
mkNotes (NTOr tn fn1 fn2 ns1 ns2)
| isStar ns1 && isStar ns2 && isDef tn && isDef fn1 && isDef fn2 = NStar
mkNotes (NTLambda tn ns1 ns2)
| isStar ns1 && isStar ns2 && isDef tn = NStar
mkNotes (NTMap tn kn vns)
| isStar vns && isDef tn && isDef kn = NStar
mkNotes (NTc t) | isDef t = NStar
mkNotes (NTKey t) | isDef t = NStar
mkNotes (NTUnit t) | isDef t = NStar
mkNotes (NTSignature t) | isDef t = NStar
mkNotes (NTOperation t) | isDef t = NStar
mkNotes n = N n
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' (NTOption a f n) (NTOption b g m) =
NTOption <$> convergeAnns a b <*> convergeAnns f g <*> 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
converge :: Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge NStar a = pure a
converge a NStar = pure a
converge (N a) (N b) = N <$> converge' a b
data AnnConvergeError where
AnnConvergeError
:: forall (tag :: Kind.Type).
(Buildable (Annotation tag), Show (Annotation tag), Typeable tag)
=> Annotation tag -> Annotation tag -> AnnConvergeError
deriving 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