TypeAnns.hs

-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

{-# LANGUAGE UndecidableSuperClasses #-}

-- | Type annotations for Lorentz types.
module Lorentz.TypeAnns
  ( HasTypeAnn (..)
  , GHasTypeAnn (..)
  , insertTypeAnn
  ) where

import Data.Singletons (SingI)
import qualified GHC.Generics as G
import Named (NamedF)

import Michelson.Text
import Michelson.Typed
  (BigMap, ContractRef(..), EpAddress, Notes(..), Operation, ToT, insertTypeAnn, starNotes)
import Michelson.Typed.Haskell.Value (GValueType)
import Michelson.Untyped (TypeAnn, ann, noAnn)
import Tezos.Address
import Tezos.Core
import Tezos.Crypto
import Util.TypeLits

-- For supporting type annotations of entrypoint arguments.
--
--At the botton of this infra is the HasTypeAnn class, which defines the type
--annotations for a given type. Right now the type annotations can only come
--from names in a named field. That is, we are not deriving names from, for
--example, record field names.

class HasTypeAnn a where
  getTypeAnn :: Notes (ToT a)

  default getTypeAnn
    :: (GHasTypeAnn (G.Rep a), GValueType (G.Rep a) ~ ToT a) => Notes (ToT a)
  getTypeAnn = gGetTypeAnn @(G.Rep a)

instance (HasTypeAnn a, KnownSymbol name)
  => HasTypeAnn (NamedF Identity a name) where
  getTypeAnn = insertTypeAnn (symbolAnn @name) $ getTypeAnn @a
    where
      symbolAnn :: forall s. KnownSymbol s => TypeAnn
      symbolAnn = ann $ symbolValT' @s

instance (HasTypeAnn (Maybe a), KnownSymbol name)
  => HasTypeAnn (NamedF Maybe a name) where
  getTypeAnn = getTypeAnn @(NamedF Identity (Maybe a) name)

-- Primitive instances
instance (HasTypeAnn a) => HasTypeAnn (Maybe a) where
  getTypeAnn = NTOption noAnn (getTypeAnn @a)

instance HasTypeAnn ()

instance HasTypeAnn Integer where
  getTypeAnn = starNotes

instance HasTypeAnn Natural where
  getTypeAnn = starNotes

instance HasTypeAnn MText where
  getTypeAnn = starNotes

instance HasTypeAnn Bool where
  getTypeAnn = starNotes

instance HasTypeAnn ByteString where
  getTypeAnn = starNotes

instance HasTypeAnn Mutez where
  getTypeAnn = starNotes

instance HasTypeAnn Address where
  getTypeAnn = starNotes

instance HasTypeAnn EpAddress where
  getTypeAnn = starNotes

instance HasTypeAnn KeyHash where
  getTypeAnn = starNotes

instance HasTypeAnn Timestamp where
  getTypeAnn = starNotes

instance HasTypeAnn PublicKey where
  getTypeAnn = starNotes

instance HasTypeAnn Signature where
  getTypeAnn = starNotes

instance (HasTypeAnn a) => HasTypeAnn (ContractRef a) where
  getTypeAnn = NTContract noAnn (getTypeAnn @a)

instance (HasTypeAnn k, HasTypeAnn v) => HasTypeAnn (Map k v) where
  getTypeAnn = NTMap noAnn (getTypeAnn @k) (getTypeAnn @v)

instance (HasTypeAnn k, HasTypeAnn v) => HasTypeAnn (BigMap k v) where
  getTypeAnn = NTBigMap noAnn (getTypeAnn @k) (getTypeAnn @v)

instance (SingI (ToT v), Typeable (ToT v)) => HasTypeAnn (Set v) where
  getTypeAnn = starNotes

instance (HasTypeAnn a) => HasTypeAnn [a] where
  getTypeAnn = NTList noAnn (getTypeAnn @a)

instance HasTypeAnn Operation where
  getTypeAnn = starNotes

instance (HasTypeAnn a, HasTypeAnn b) => HasTypeAnn (a, b)
instance (HasTypeAnn a, HasTypeAnn b, HasTypeAnn c) => HasTypeAnn (a, b, c)
instance (HasTypeAnn a, HasTypeAnn b, HasTypeAnn c, HasTypeAnn d) => HasTypeAnn (a, b, c, d)
instance (HasTypeAnn a, HasTypeAnn b, HasTypeAnn c, HasTypeAnn d, HasTypeAnn e)
  => HasTypeAnn (a, b, c, d, e)
instance (HasTypeAnn a, HasTypeAnn b, HasTypeAnn c, HasTypeAnn d, HasTypeAnn e, HasTypeAnn f)
  => HasTypeAnn (a, b, c, d, e, f)
instance
  ( HasTypeAnn a, HasTypeAnn b, HasTypeAnn c, HasTypeAnn d, HasTypeAnn e
  , HasTypeAnn f, HasTypeAnn g)
  => HasTypeAnn (a, b, c, d, e, f, g)

-- A Generic HasTypeAnn implementation
class GHasTypeAnn a where
  gGetTypeAnn :: Notes (GValueType a)

instance GHasTypeAnn G.U1 where
  gGetTypeAnn = starNotes

instance (GHasTypeAnn x) => GHasTypeAnn (G.M1 i0 i1 x) where
  gGetTypeAnn = gGetTypeAnn @x

instance
    ( GHasTypeAnn x
    , GHasTypeAnn y
    )
  =>
    GHasTypeAnn (x G.:+: y)
  where
  gGetTypeAnn = NTOr noAnn noAnn noAnn
    (gGetTypeAnn @x)
    (gGetTypeAnn @y)

instance
    ( GHasTypeAnn x
    , GHasTypeAnn y
    )
  =>
    GHasTypeAnn (x G.:*: y)
  where
  gGetTypeAnn = NTPair noAnn noAnn noAnn
    (gGetTypeAnn @x)
    (gGetTypeAnn @y)

instance (HasTypeAnn x) => GHasTypeAnn (G.Rec0 x) where
  gGetTypeAnn = getTypeAnn @x