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

{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Conversions between haskell types/values and Michelson ones.
module Michelson.Typed.Haskell.Value
  ( -- * Value conversions
    IsoValue (..)
  , KnownIsoT
  , KnownT
  , GIsoValue (GValueType)
  , ToT'
  , SomeIsoValue (..)
  , AnyIsoValue (..)
  , GenericIsoValue
  , WellTyped
  , WellTypedIsoValue
  , WellTypedToT

  , Dict(..) -- * Re-exporting to use in tests.

    -- * Missing Haskell analogies to Michelson values
  , EntrypointCall
  , SomeEntrypointCall
  , ContractRef (..)
  , coerceContractRef
  , contractRefToAddr
  , BigMap (..)

    -- * Stack conversion
  , ToTs
  , ToTs'
  , IsoValuesStack (..)
  , totsKnownLemma
  , totsAppendLemma
  ) where

import Data.Constraint ((:-)(..), Dict(..))
import Data.Default (Default(..))
import qualified Data.Kind as Kind
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Data.Vinyl.Core (Rec(..))
import Fmt (Buildable(..))
import GHC.Generics ((:*:)(..), (:+:)(..))
import qualified GHC.Generics as G
import Named (NamedF(..))

import Michelson.Text
import Michelson.Typed.Aliases
import Michelson.Typed.Entrypoints
import Michelson.Typed.Sing
import Michelson.Typed.T
import Michelson.Typed.Value
import Tezos.Address (Address)
import Tezos.Core (ChainId, Mutez, Timestamp)
import Tezos.Crypto (KeyHash, PublicKey, Signature)
import Util.Type

----------------------------------------------------------------------------
-- Complex values isomorphism
----------------------------------------------------------------------------

type KnownIsoT a = KnownT (ToT a)

-- | Isomorphism between Michelson values and plain Haskell types.
--
-- Default implementation of this typeclass converts ADTs to Michelson
-- "pair"s and "or"s.
class (WellTypedToT a) => IsoValue a where
  -- | Type function that converts a regular Haskell type into a @T@ type.
  type ToT a :: T
  type ToT a = GValueType (G.Rep a)

  -- | Converts a Haskell structure into @Value@ representation.
  toVal :: a -> Value (ToT a)
  default toVal
    :: (Generic a, GIsoValue (G.Rep a), ToT a ~ GValueType (G.Rep a))
    => a -> Value (ToT a)
  toVal = gToValue . G.from

  -- | Converts a @Value@ into Haskell type.
  fromVal :: Value (ToT a) -> a
  default fromVal
    :: (Generic a, GIsoValue (G.Rep a), ToT a ~ GValueType (G.Rep a))
    => Value (ToT a) -> a
  fromVal = G.to . gFromValue

-- | Overloaded version of 'ToT' to work on Haskell and @T@ types.
type family ToT' (t :: k) :: T where
  ToT' (t :: T) = t
  ToT' (t :: Kind.Type) = ToT t

-- | Hides some Haskell value put in line with Michelson 'Value'.
data SomeIsoValue where
  SomeIsoValue :: (KnownIsoT a) => a -> SomeIsoValue

-- | Any Haskell value which can be converted to Michelson 'Value'.
newtype AnyIsoValue = AnyIsoValue (forall a. IsoValue a => a)

-- Instances
----------------------------------------------------------------------------

instance IsoValue Integer where
  type ToT Integer = 'TInt
  toVal = VInt
  fromVal (VInt x) = x

instance IsoValue Natural where
  type ToT Natural = 'TNat
  toVal = VNat
  fromVal (VNat x) = x

instance IsoValue MText where
  type ToT MText = 'TString
  toVal = VString
  fromVal (VString x) = x

instance DoNotUseTextError => IsoValue Text where
  type ToT Text = ToT MText
  toVal = error "impossible"
  fromVal = error "impossible"

instance IsoValue Bool where
  type ToT Bool = 'TBool
  toVal = VBool
  fromVal (VBool x) = x

instance IsoValue ByteString where
  type ToT ByteString = 'TBytes
  toVal = VBytes
  fromVal (VBytes x) = x

instance IsoValue Mutez where
  type ToT Mutez = 'TMutez
  toVal = VMutez
  fromVal (VMutez x) = x

instance IsoValue KeyHash where
  type ToT KeyHash = 'TKeyHash
  toVal = VKeyHash
  fromVal (VKeyHash x) = x

instance IsoValue Timestamp where
  type ToT Timestamp = 'TTimestamp
  toVal = VTimestamp
  fromVal (VTimestamp x) = x

instance IsoValue Address where
  type ToT Address = 'TAddress
  toVal addr = VAddress $ EpAddress addr DefEpName
  fromVal (VAddress x) = eaAddress x

instance IsoValue EpAddress where
  type ToT EpAddress = 'TAddress
  toVal = VAddress
  fromVal (VAddress x) = x

instance IsoValue PublicKey where
  type ToT PublicKey = 'TKey
  toVal = VKey
  fromVal (VKey x) = x

instance IsoValue Signature where
  type ToT Signature = 'TSignature
  toVal = VSignature
  fromVal (VSignature x) = x

instance IsoValue ChainId where
  type ToT ChainId = 'TChainId
  toVal = VChainId
  fromVal (VChainId x) = x

instance IsoValue ()

instance IsoValue a => IsoValue [a] where
  type ToT [a] = 'TList (ToT a)
  toVal = VList . map toVal
  fromVal (VList x) = map fromVal x

instance IsoValue a => IsoValue (Maybe a) where
  type ToT (Maybe a) = 'TOption (ToT a)
  toVal = VOption . fmap toVal
  fromVal (VOption x) = fmap fromVal x

instance (IsoValue l, IsoValue r) => IsoValue (Either l r)

instance (IsoValue a, IsoValue b) => IsoValue (a, b)

instance (Comparable (ToT c), Ord c, IsoValue c) => IsoValue (Set c) where
  type ToT (Set c) = 'TSet (ToT c)
  toVal = VSet . Set.map toVal
  fromVal (VSet x) = Set.map fromVal x

instance (Comparable (ToT k), Ord k, IsoValue k, IsoValue v) => IsoValue (Map k v) where
  type ToT (Map k v) = 'TMap (ToT k) (ToT v)
  toVal = VMap . Map.mapKeys toVal . Map.map toVal
  fromVal (VMap x) = Map.map fromVal $ Map.mapKeys fromVal x

instance IsoValue Operation where
  type ToT Operation = 'TOperation
  toVal = VOp
  fromVal (VOp x) = x

deriving newtype instance IsoValue a => IsoValue (Identity a)
deriving newtype instance IsoValue a => IsoValue (NamedF Identity a name)
deriving newtype instance IsoValue a => IsoValue (NamedF Maybe a name)

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

-- Types used specifically for conversion
----------------------------------------------------------------------------

type EntrypointCall param arg = EntrypointCallT (ToT param) (ToT arg)

type SomeEntrypointCall arg = SomeEntrypointCallT (ToT arg)

type WellTypedToT a = WellTyped (ToT a)
type WellTypedIsoValue a = (WellTyped (ToT a), IsoValue a)

-- | Since @Contract@ name is used to designate contract code, lets call
-- analogy of 'TContract' type as follows.
--
-- Note that type argument always designates an argument of entrypoint.
-- If a contract has explicit default entrypoint (and no root entrypoint),
-- @ContractRef@ referring to it can never have the entire parameter as its
-- type argument.
data ContractRef (arg :: Kind.Type) = ContractRef
  { crAddress :: Address
  , crEntrypoint :: SomeEntrypointCall arg
  } deriving stock (Eq, Show)

instance (WellTypedToT arg) => Buildable (ContractRef arg) where
  build = buildVContract . toVal

instance (WellTypedToT arg) => IsoValue (ContractRef arg) where
  type ToT (ContractRef arg) = 'TContract (ToT arg)
  toVal ContractRef{..} = VContract crAddress crEntrypoint
  fromVal (VContract addr epc) = ContractRef addr epc

-- | Replace type argument of 'ContractAddr' with isomorphic one.
coerceContractRef :: (ToT a ~ ToT b) => ContractRef a -> ContractRef b
coerceContractRef ContractRef{..} = ContractRef{..}

contractRefToAddr :: ContractRef cp -> EpAddress
contractRefToAddr ContractRef{..} = EpAddress crAddress (sepcName crEntrypoint)

newtype BigMap k v = BigMap { unBigMap :: Map k v }
  deriving stock (Eq, Show)
  deriving newtype (Default, Semigroup, Monoid)

instance
  ( WellTypedToT k, WellTypedToT v, Comparable (ToT k)
  , Ord k, IsoValue k, IsoValue v
  ) => IsoValue (BigMap k v) where
  type ToT (BigMap k v) = 'TBigMap (ToT k) (ToT v)
  toVal = VBigMap . Map.mapKeys toVal . Map.map toVal . unBigMap
  fromVal (VBigMap x) = BigMap $ Map.map fromVal $ Map.mapKeys fromVal x

-- Generic magic
----------------------------------------------------------------------------

-- | Implements ADT conversion to Michelson value.
--
-- Thanks to Generic, Michelson representation will
-- be a balanced tree; this reduces average access time in general case.
--
-- A drawback of such approach is that, in theory, in new GHC version
-- generified representation may change; however, chances are small and
-- I (martoon) believe that contract versions will change much faster anyway.
--
-- In case an unbalanced tree is needed, the Generic instance can be derived by
-- using the utilities in the 'Util.Generics' module.
class KnownT (GValueType x) =>
      GIsoValue (x :: Kind.Type -> Kind.Type) where
  type GValueType x :: T
  gToValue :: x p -> Value (GValueType x)
  gFromValue :: Value (GValueType x) -> x p

instance GIsoValue x => GIsoValue (G.M1 t i x) where
  type GValueType (G.M1 t i x) = GValueType x
  gToValue = gToValue . G.unM1
  gFromValue = G.M1 . gFromValue

instance (GIsoValue x, GIsoValue y) => GIsoValue (x :+: y) where
  type GValueType (x :+: y) = 'TOr (GValueType x) (GValueType y)
  gToValue = VOr . \case
    L1 x -> Left (gToValue x)
    R1 y -> Right (gToValue y)
  gFromValue (VOr e) = case e of
    Left vx -> L1 (gFromValue vx)
    Right vy -> R1 (gFromValue vy)

instance (GIsoValue x, GIsoValue y) => GIsoValue (x :*: y) where
  type GValueType (x :*: y) = 'TPair (GValueType x) (GValueType y)
  gToValue (x :*: y) = VPair (gToValue x, gToValue y)
  gFromValue (VPair (vx, vy)) = gFromValue vx :*: gFromValue vy

instance GIsoValue G.U1 where
  type GValueType G.U1 = 'TUnit
  gToValue G.U1 = VUnit
  gFromValue VUnit = G.U1

instance IsoValue a => GIsoValue (G.Rec0 a) where
  type GValueType (G.Rec0 a) = ToT a
  gToValue = toVal . G.unK1
  gFromValue = G.K1 . fromVal

-- | Whether Michelson representation of the type is derived via Generics.
type GenericIsoValue t =
  (IsoValue t, Generic t, ToT t ~ GValueType (G.Rep t))

----------------------------------------------------------------------------
-- Stacks conversion
----------------------------------------------------------------------------

-- | Type function to convert a Haskell stack type to @T@-based one.
type family ToTs (ts :: [Kind.Type]) :: [T] where
  ToTs '[] = '[]
  ToTs (x ': xs) = ToT x ': ToTs xs

-- | Overloaded version of 'ToTs' to work on Haskell and @T@ stacks.
type family ToTs' (t :: [k]) :: [T] where
  ToTs' (t :: [T]) = t
  ToTs' (a :: [Kind.Type]) = ToTs a

-- | Isomorphism between Michelson stack and its Haskell reflection.
class IsoValuesStack (ts :: [Kind.Type]) where
  toValStack :: Rec Identity ts -> Rec Value (ToTs ts)
  fromValStack :: Rec Value (ToTs ts) -> Rec Identity ts

instance IsoValuesStack '[] where
  toValStack RNil = RNil
  fromValStack RNil = RNil

instance (IsoValue t, IsoValuesStack st) => IsoValuesStack (t ': st) where
  toValStack (v :& vs) = toVal v :& toValStack vs
  fromValStack (v :& vs) = fromVal v :& fromValStack vs

totsKnownLemma :: forall s. KnownList s :- KnownList (ToTs s)
totsKnownLemma = Sub $ case klist @s of
  KNil -> Dict
  KCons _ (_ :: Proxy a') ->
    case totsKnownLemma @a' of Sub Dict -> Dict

totsAppendLemma
  :: forall a b.
      (KnownList a)
  => Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
totsAppendLemma = case klist @a of
  KNil -> Dict
  KCons _ (_ :: Proxy a') ->
    case totsAppendLemma @a' @b of Dict -> Dict

-- | This class encodes Michelson rules w.r.t where it requires comparable
-- types. Earlier we had a dedicated type for representing comparable types @CT@.
-- But then we integreated those types into @T@. This meant that some of the
-- types that could be formed with various combinations of @T@ would be
-- illegal as per Michelson typing rule. Using this class, we inductively
-- enforce that a type and all types it contains are well typed as per
-- Michelson's rules.
class (KnownT t, WellTypedSuperC t) => WellTyped (t :: T) where
  -- | Constraints required for instance of a given type.
  type WellTypedSuperC t :: Constraint
  type WellTypedSuperC t = ()

instance WellTyped 'TKey where
instance WellTyped 'TUnit where
instance WellTyped 'TSignature where
instance WellTyped 'TChainId where
instance WellTyped t => WellTyped ('TOption t) where
  type WellTypedSuperC ('TOption t) = WellTyped t
instance WellTyped t => WellTyped ('TList t) where
  type WellTypedSuperC ('TList t) = WellTyped t
instance (Comparable t, WellTyped t) => WellTyped ('TSet t) where
  type WellTypedSuperC ('TSet t) = (Comparable t, WellTyped t)
instance WellTyped 'TOperation where
instance WellTyped t => WellTyped ('TContract t) where
  type WellTypedSuperC ('TContract t) = WellTyped t
instance (WellTyped t1, WellTyped t2) => WellTyped ('TPair t1 t2) where
  type WellTypedSuperC ('TPair t1 t2) = (WellTyped t1, WellTyped t2)
instance (WellTyped t1, WellTyped t2) => WellTyped ('TOr t1 t2) where
  type WellTypedSuperC ('TOr t1 t2) = (WellTyped t1, WellTyped t2)
instance (WellTyped t1, WellTyped t2) => WellTyped ('TLambda t1 t2) where
  type WellTypedSuperC ('TLambda t1 t2) = (WellTyped t1, WellTyped t2)
instance (Comparable k, WellTyped k, WellTyped v) => WellTyped ('TMap k v) where
  type WellTypedSuperC ('TMap k v) = (Comparable k, WellTyped k, WellTyped v)
instance (Comparable k, WellTyped k, WellTyped v) => WellTyped ('TBigMap k v) where
  type WellTypedSuperC ('TBigMap k v) = (Comparable k, WellTyped k, WellTyped v)
instance WellTyped 'TInt
instance WellTyped 'TNat
instance WellTyped 'TString
instance WellTyped 'TBytes
instance WellTyped 'TMutez
instance WellTyped 'TBool
instance WellTyped 'TKeyHash
instance WellTyped 'TTimestamp
instance WellTyped 'TAddress