Annotation.hs

{-# LANGUAGE DataKinds, GADTs #-}

-- | Module, providing @Notes t@ data type, which holds annotations for a
-- given type @t@.
--
-- Annotation type @Notes t@ is a tree, each leaf is either a star (@*@) or a
-- constructor holding some annotation data for a given type @t@.
-- Star corresponds to the case when given Michelson type contains no
-- annotations.
--
-- This module also provides type class 'Converge' along with some
-- utility functions which are used to combine two annotations trees
-- `a` and `b` into a new one `c` in such a way that `c` can be obtained from
-- both `a` and `b` by replacing some @*@ leafs with type or/and field
-- annotations.

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 type, holding annotation data for a given Michelson type @t@.
--
-- Each constructor corresponds to exactly one constructor of 'T'
-- and holds all type and field annotations that can be attributed to a
-- Michelson type corrspoding to @t@.
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 instance Show (Notes t)
deriving instance Eq (Notes t)

-- | In memory of `NStar` constructor.
--   Generates notes with no annotations.
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

-- | Checks if no annotations are present.
isStar :: SingI t => Notes t -> Bool
isStar = (== starNotes)

orAnn :: Annotation t -> Annotation t -> Annotation t
orAnn a b = bool a b (a == def)

-- | Combines two annotations trees `a` and `b` into a new one `c`
-- in such a way that `c` can be obtained from both `a` and `b` by replacing
-- some empty leaves with type or/and field annotations.
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 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 |+ ""

-- | Converge two type or field notes (which may be wildcards).
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