-- 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 qualified GHC.Generics as G
import Named (NamedF)

import Michelson.Text
import Michelson.Typed
  (BigMap, ContractRef(..), EpAddress, KnownIsoT, 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 = GHasTypeAnn (Rep a) => Notes (GValueType (Rep a))
forall (a :: * -> *). GHasTypeAnn a => Notes (GValueType a)
gGetTypeAnn @(G.Rep a)

instance (HasTypeAnn a, KnownSymbol name)
  => HasTypeAnn (NamedF Identity a name) where
  getTypeAnn :: Notes (ToT (NamedF Identity a name))
getTypeAnn = TypeAnn -> Notes (ToT a) -> Notes (ToT a)
forall (b :: T). TypeAnn -> Notes b -> Notes b
insertTypeAnn (KnownSymbol name => TypeAnn
forall (s :: Symbol). KnownSymbol s => TypeAnn
symbolAnn @name) (Notes (ToT a) -> Notes (ToT (NamedF Identity a name)))
-> Notes (ToT a) -> Notes (ToT (NamedF Identity a name))
forall a b. (a -> b) -> a -> b
$ HasTypeAnn a => Notes (ToT a)
forall a. HasTypeAnn a => Notes (ToT a)
getTypeAnn @a
    where
      symbolAnn :: forall s. KnownSymbol s => TypeAnn
      symbolAnn :: TypeAnn
symbolAnn = Text -> TypeAnn
forall k (a :: k). HasCallStack => Text -> Annotation a
ann (Text -> TypeAnn) -> Text -> TypeAnn
forall a b. (a -> b) -> a -> b
$ KnownSymbol s => Text
forall (s :: Symbol). KnownSymbol s => Text
symbolValT' @s

instance (HasTypeAnn (Maybe a), KnownSymbol name)
  => HasTypeAnn (NamedF Maybe a name) where
  getTypeAnn :: Notes (ToT (NamedF Maybe a name))
getTypeAnn = HasTypeAnn (NamedF Identity (Maybe a) name) =>
Notes (ToT (NamedF Identity (Maybe a) name))
forall a. HasTypeAnn a => Notes (ToT a)
getTypeAnn @(NamedF Identity (Maybe a) name)

-- Primitive instances
instance (HasTypeAnn a) => HasTypeAnn (Maybe a) where
  getTypeAnn :: Notes (ToT (Maybe a))
getTypeAnn = TypeAnn -> Notes (ToT a) -> Notes ('TOption (ToT a))
forall (t1 :: T). TypeAnn -> Notes t1 -> Notes ('TOption t1)
NTOption TypeAnn
forall k (a :: k). Annotation a
noAnn (HasTypeAnn a => Notes (ToT a)
forall a. HasTypeAnn a => Notes (ToT a)
getTypeAnn @a)

instance HasTypeAnn ()

instance HasTypeAnn Integer where
  getTypeAnn :: Notes (ToT Integer)
getTypeAnn = Notes (ToT Integer)
forall (t :: T). SingI t => Notes t
starNotes

instance HasTypeAnn Natural where
  getTypeAnn :: Notes (ToT Natural)
getTypeAnn = Notes (ToT Natural)
forall (t :: T). SingI t => Notes t
starNotes

instance HasTypeAnn MText where
  getTypeAnn :: Notes (ToT MText)
getTypeAnn = Notes (ToT MText)
forall (t :: T). SingI t => Notes t
starNotes

instance HasTypeAnn Bool where
  getTypeAnn :: Notes (ToT Bool)
getTypeAnn = Notes (ToT Bool)
forall (t :: T). SingI t => Notes t
starNotes

instance HasTypeAnn ByteString where
  getTypeAnn :: Notes (ToT ByteString)
getTypeAnn = Notes (ToT ByteString)
forall (t :: T). SingI t => Notes t
starNotes

instance HasTypeAnn Mutez where
  getTypeAnn :: Notes (ToT Mutez)
getTypeAnn = Notes (ToT Mutez)
forall (t :: T). SingI t => Notes t
starNotes

instance HasTypeAnn Address where
  getTypeAnn :: Notes (ToT Address)
getTypeAnn = Notes (ToT Address)
forall (t :: T). SingI t => Notes t
starNotes

instance HasTypeAnn EpAddress where
  getTypeAnn :: Notes (ToT EpAddress)
getTypeAnn = Notes (ToT EpAddress)
forall (t :: T). SingI t => Notes t
starNotes

instance HasTypeAnn KeyHash where
  getTypeAnn :: Notes (ToT KeyHash)
getTypeAnn = Notes (ToT KeyHash)
forall (t :: T). SingI t => Notes t
starNotes

instance HasTypeAnn Timestamp where
  getTypeAnn :: Notes (ToT Timestamp)
getTypeAnn = Notes (ToT Timestamp)
forall (t :: T). SingI t => Notes t
starNotes

instance HasTypeAnn PublicKey where
  getTypeAnn :: Notes (ToT PublicKey)
getTypeAnn = Notes (ToT PublicKey)
forall (t :: T). SingI t => Notes t
starNotes

instance HasTypeAnn Signature where
  getTypeAnn :: Notes (ToT Signature)
getTypeAnn = Notes (ToT Signature)
forall (t :: T). SingI t => Notes t
starNotes

instance (HasTypeAnn a) => HasTypeAnn (ContractRef a) where
  getTypeAnn :: Notes (ToT (ContractRef a))
getTypeAnn = TypeAnn -> Notes (ToT a) -> Notes ('TContract (ToT a))
forall (t1 :: T). TypeAnn -> Notes t1 -> Notes ('TContract t1)
NTContract TypeAnn
forall k (a :: k). Annotation a
noAnn (HasTypeAnn a => Notes (ToT a)
forall a. HasTypeAnn a => Notes (ToT a)
getTypeAnn @a)

instance (HasTypeAnn k, HasTypeAnn v) => HasTypeAnn (Map k v) where
  getTypeAnn :: Notes (ToT (Map k v))
getTypeAnn = TypeAnn
-> Notes (ToT k) -> Notes (ToT v) -> Notes ('TMap (ToT k) (ToT v))
forall (k :: T) (v :: T).
TypeAnn -> Notes k -> Notes v -> Notes ('TMap k v)
NTMap TypeAnn
forall k (a :: k). Annotation a
noAnn (HasTypeAnn k => Notes (ToT k)
forall a. HasTypeAnn a => Notes (ToT a)
getTypeAnn @k) (HasTypeAnn v => Notes (ToT v)
forall a. HasTypeAnn a => Notes (ToT a)
getTypeAnn @v)

instance (HasTypeAnn k, HasTypeAnn v) => HasTypeAnn (BigMap k v) where
  getTypeAnn :: Notes (ToT (BigMap k v))
getTypeAnn = TypeAnn
-> Notes (ToT k)
-> Notes (ToT v)
-> Notes ('TBigMap (ToT k) (ToT v))
forall (k :: T) (v :: T).
TypeAnn -> Notes k -> Notes v -> Notes ('TBigMap k v)
NTBigMap TypeAnn
forall k (a :: k). Annotation a
noAnn (HasTypeAnn k => Notes (ToT k)
forall a. HasTypeAnn a => Notes (ToT a)
getTypeAnn @k) (HasTypeAnn v => Notes (ToT v)
forall a. HasTypeAnn a => Notes (ToT a)
getTypeAnn @v)

instance (KnownIsoT v) => HasTypeAnn (Set v) where
  getTypeAnn :: Notes (ToT (Set v))
getTypeAnn = Notes (ToT (Set v))
forall (t :: T). SingI t => Notes t
starNotes

instance (HasTypeAnn a) => HasTypeAnn [a] where
  getTypeAnn :: Notes (ToT [a])
getTypeAnn = TypeAnn -> Notes (ToT a) -> Notes ('TList (ToT a))
forall (t1 :: T). TypeAnn -> Notes t1 -> Notes ('TList t1)
NTList TypeAnn
forall k (a :: k). Annotation a
noAnn (HasTypeAnn a => Notes (ToT a)
forall a. HasTypeAnn a => Notes (ToT a)
getTypeAnn @a)

instance HasTypeAnn Operation where
  getTypeAnn :: Notes (ToT Operation)
getTypeAnn = Notes (ToT Operation)
forall (t :: T). SingI t => Notes t
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 :: Notes (GValueType U1)
gGetTypeAnn = Notes (GValueType U1)
forall (t :: T). SingI t => Notes t
starNotes

instance (GHasTypeAnn x) => GHasTypeAnn (G.M1 i0 i1 x) where
  gGetTypeAnn :: Notes (GValueType (M1 i0 i1 x))
gGetTypeAnn = GHasTypeAnn x => Notes (GValueType x)
forall (a :: * -> *). GHasTypeAnn a => Notes (GValueType a)
gGetTypeAnn @x

instance
    ( GHasTypeAnn x
    , GHasTypeAnn y
    )
  =>
    GHasTypeAnn (x G.:+: y)
  where
  gGetTypeAnn :: Notes (GValueType (x :+: y))
gGetTypeAnn = TypeAnn
-> FieldAnn
-> FieldAnn
-> Notes (GValueType x)
-> Notes (GValueType y)
-> Notes ('TOr (GValueType x) (GValueType y))
forall (p :: T) (q :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TOr p q)
NTOr TypeAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn
    (GHasTypeAnn x => Notes (GValueType x)
forall (a :: * -> *). GHasTypeAnn a => Notes (GValueType a)
gGetTypeAnn @x)
    (GHasTypeAnn y => Notes (GValueType y)
forall (a :: * -> *). GHasTypeAnn a => Notes (GValueType a)
gGetTypeAnn @y)

instance
    ( GHasTypeAnn x
    , GHasTypeAnn y
    )
  =>
    GHasTypeAnn (x G.:*: y)
  where
  gGetTypeAnn :: Notes (GValueType (x :*: y))
gGetTypeAnn = TypeAnn
-> FieldAnn
-> FieldAnn
-> Notes (GValueType x)
-> Notes (GValueType y)
-> Notes ('TPair (GValueType x) (GValueType y))
forall (p :: T) (q :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TPair p q)
NTPair TypeAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn
    (GHasTypeAnn x => Notes (GValueType x)
forall (a :: * -> *). GHasTypeAnn a => Notes (GValueType a)
gGetTypeAnn @x)
    (GHasTypeAnn y => Notes (GValueType y)
forall (a :: * -> *). GHasTypeAnn a => Notes (GValueType a)
gGetTypeAnn @y)

instance (HasTypeAnn x) => GHasTypeAnn (G.Rec0 x) where
  gGetTypeAnn :: Notes (GValueType (Rec0 x))
gGetTypeAnn = HasTypeAnn x => Notes (ToT x)
forall a. HasTypeAnn a => Notes (ToT a)
getTypeAnn @x