-- 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 Morley.Michelson.Typed.Haskell.Value
  ( -- * Value conversions
    IsoValue (..)
  , KnownIsoT
  , GIsoValue (GValueType)
  , ToT'
  , GenericIsoValue
  , WellTyped
  , WellTypedIsoValue
  , WellTypedToT
  , HasNoOpToT

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

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

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

import Data.Constraint (Dict(..))
import Data.Data (Data)
import Data.Default (Default(..))
import Data.Fixed (Fixed(..))
import Data.Foldable (Foldable(foldr))
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Data.Vinyl.Core (Rec(..))
import Fmt (Buildable(..), mapF)
import GHC.Exts as Exts (IsList(..))
import GHC.Generics ((:*:)(..), (:+:)(..))
import qualified GHC.Generics as G

import Morley.Michelson.Text
import Morley.Michelson.Typed.Aliases
import Morley.Michelson.Typed.Entrypoints
import Morley.Michelson.Typed.Scope
import Morley.Michelson.Typed.T
import Morley.Michelson.Typed.Value
import Morley.Tezos.Address (Address)
import Morley.Tezos.Core (ChainId, Mutez, Timestamp)
import Morley.Tezos.Crypto (Bls12381Fr, Bls12381G1, Bls12381G2, KeyHash, PublicKey, Signature)
import Morley.Util.Named
import Morley.Util.Type

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

type KnownIsoT a = SingI (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 :: Type) = ToT t

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

instance WellTyped t => IsoValue (Value t) where
  type ToT (Value t) = t
  toVal = id
  fromVal = id

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 Bls12381Fr where
  type ToT Bls12381Fr = 'TBls12381Fr
  toVal = VBls12381Fr
  fromVal (VBls12381Fr x) = x

instance IsoValue Bls12381G1 where
  type ToT Bls12381G1 = 'TBls12381G1
  toVal = VBls12381G1
  fromVal (VBls12381G1 x) = x

instance IsoValue Bls12381G2 where
  type ToT Bls12381G2 = 'TBls12381G2
  toVal = VBls12381G2
  fromVal (VBls12381G2 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 (Fixed p) where
  type ToT (Fixed p) = 'TInt
  toVal (MkFixed x) = VInt x
  fromVal (VInt x) = MkFixed 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 Void

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)

type HasNoOpToT a = HasNoOp (ToT a)
type HasNoBigMapToT a = HasNoBigMap (ToT 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 :: Type) = ContractRef
  { crAddress :: Address
  , crEntrypoint :: SomeEntrypointCall arg
  } deriving stock (Eq, Show)

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

instance (HasNoOpToT arg, 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 'ContractRef' 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)

-- | Ticket type.
data Ticket (arg :: Type) = Ticket
  { tTicketer :: Address
  , tData :: arg
  , tAmount :: Natural
  } deriving stock (Eq, Show)

instance (Comparable (ToT a), IsoValue a) => IsoValue (Ticket a) where
  type ToT (Ticket a) = 'TTicket (ToT a)
  toVal Ticket{..} = VTicket tTicketer (toVal tData) tAmount
  fromVal (VTicket tTicketer dat tAmount) = Ticket{ tData = fromVal dat, .. }

-- | Phantom type that represents the ID of a big_map with
-- keys of type @k@ and values of type @v@.
newtype BigMapId k v = BigMapId { unBigMapId :: Natural }
  -- Note: we purposefully do not derive an `Eq` instance.
  -- If we did, it would be possible for a @cleveland@ user to mistakenly
  -- compare two big_map IDs, whilst being under the impression that they were
  -- actually comparing the big_map's contents.
  -- To avoid this confusion, we simply do not create an `Eq` instance.
  -- For context, see: https://gitlab.com/morley-framework/morley/-/merge_requests/833#note_598577341
  deriving stock (Show, Data)
  deriving newtype (IsoValue, Buildable, Num)

data BigMap k v = BigMap
  { bmId :: Maybe (BigMapId k v)
  , bmMap :: Map k v
  }
  deriving stock (Show, Generic, Data)
  deriving anyclass (Default, Container)

class ToBigMap m where
  type ToBigMapKey m
  type ToBigMapValue m
  mkBigMap :: m -> BigMap (ToBigMapKey m) (ToBigMapValue m)

instance Ord k => ToBigMap [(k, v)] where
  type ToBigMapValue [(k, v)] = v
  type ToBigMapKey [(k, v)] = k
  mkBigMap = Exts.fromList

instance ToBigMap (Map k v) where
  type ToBigMapValue (Map k v) = v
  type ToBigMapKey (Map k v) = k
  mkBigMap = BigMap Nothing

instance Ord k => ToBigMap (NonEmpty (k, v)) where
  type ToBigMapValue (NonEmpty (k, v)) = v
  type ToBigMapKey (NonEmpty (k, v)) = k
  mkBigMap (h :| t) = one h <> mkBigMap t

instance Ord k => Semigroup (BigMap k v) where
  BigMap _ m1 <> BigMap _ m2 = BigMap Nothing (m1 <> m2)

instance Foldable (BigMap k) where
  foldr f z (BigMap _ bmMap) = Map.foldr f z bmMap

instance One (BigMap k v) where
  type OneItem (BigMap k v) = OneItem (Map k v)
  one x = BigMap Nothing (one x)

instance Ord k => IsList (BigMap k v) where
  type Item (BigMap k v) = Item (Map k v)
  fromList xs = BigMap Nothing (Exts.fromList xs)
  toList (BigMap _ xs) = Exts.toList xs

instance (Ord k, Buildable k, Buildable v) => Buildable (BigMap k v) where
  build = mapF

instance
  ( Comparable (ToT k) , Ord k, IsoValue k
  , IsoValue v, HasNoBigMapToT v, HasNoOpToT v
  ) => IsoValue (BigMap k v) where
  type ToT (BigMap k v) = 'TBigMap (ToT k) (ToT v)
  toVal (BigMap bmId bmMap) =
    VBigMap
      (unBigMapId <$> bmId)
      (Map.mapKeys toVal $ Map.map toVal bmMap)
  fromVal (VBigMap bmId x) =
    BigMap
      (BigMapId <$> bmId)
      (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 "Morley.Util.Generic" module.
class SingI (GValueType x) =>
      GIsoValue (x :: Type -> 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 GIsoValue G.V1 where
  type GValueType G.V1 = 'TNever
  gToValue = \case
  gFromValue = \case

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 :: [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 :: [Type]) = ToTs a

-- | Isomorphism between Michelson stack and its Haskell reflection.
class IsoValuesStack (ts :: [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 (SingI t, WellTypedSuperC t) => WellTyped (t :: T) where
  -- | Constraints required for instance of a given type.
  type WellTypedSuperC t :: Constraint
  type WellTypedSuperC _ = ()

instance WellTyped 'TKey where
instance WellTyped 'TUnit where
instance WellTyped 'TNever 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, HasNoOp t) => WellTyped ('TContract t) where
  type WellTypedSuperC ('TContract t) = (WellTyped t, HasNoOp t)
instance (WellTyped t, Comparable t) => WellTyped ('TTicket t) where
  type WellTypedSuperC ('TTicket t) = (WellTyped t, Comparable 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, HasNoBigMap v, HasNoOp v)
         => WellTyped ('TBigMap k v) where
  type WellTypedSuperC ('TBigMap k v) = ( Comparable k, WellTyped k, WellTyped v
                                        , HasNoBigMap v, HasNoOp v)
instance WellTyped 'TInt
instance WellTyped 'TNat
instance WellTyped 'TString
instance WellTyped 'TBytes
instance WellTyped 'TMutez
instance WellTyped 'TBool
instance WellTyped 'TKeyHash
instance WellTyped 'TBls12381Fr
instance WellTyped 'TBls12381G1
instance WellTyped 'TBls12381G2
instance WellTyped 'TTimestamp
instance WellTyped 'TAddress