-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

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

-- | Conversions between haskell types/values and Michelson ones.
module Morley.Michelson.Typed.Haskell.Value
  ( -- * Value conversions
    IsoValue (..)
  , isoValue
  , KnownIsoT
  , GIsoValue (GValueType)
  , ToT'
  , GenericIsoValue
  , 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 Control.Lens (At(..), Index, Iso, IxValue, Ixed(..), iso)
import Data.Constraint (Bottom(..), Dict(..))
import Data.Data (Data)
import Data.Default (Default(..))
import Data.Fixed (Fixed(..))
import Data.Foldable (Foldable(foldr))
import Data.Map.Strict qualified as Map
import Data.Set qualified as Set
import Data.Vinyl.Core (Rec(..))
import Fmt (Buildable(..), mapF)
import GHC.Exts as Exts (IsList(..))
import GHC.Generics ((:*:)(..), (:+:)(..))
import GHC.Generics qualified 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
import Morley.Tezos.Core (ChainId, Mutez, Timestamp)
import Morley.Tezos.Crypto
  (Bls12381Fr, Bls12381G1, Bls12381G2, Chest, ChestKey, KeyHash, PublicKey, Signature)
import Morley.Util.Named
import Morley.Util.SizedList.Types
import Morley.Util.Type

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

type KnownIsoT a = (IsoValue 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 ToT' :: forall k. k -> T
type family ToT' t where
  ToT' (t :: T) = t
  ToT' (t :: Type) = ToT t

-- | An optic witnessing the isomorphism between a michelson type and a haskell type.
isoValue :: (IsoValue a, IsoValue b) => Iso (Value (ToT a)) (Value (ToT b)) a b
isoValue = iso fromVal toVal

-- 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 (Bottom, DoNotUseTextError) => IsoValue Text where
  type ToT Text = ToT MText
  toVal = no
  fromVal = no

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

instance IsoValue Chest where
  type ToT Chest = 'TChest
  toVal = VChest
  fromVal (VChest x) = x

instance IsoValue ChestKey where
  type ToT ChestKey = 'TChestKey
  toVal = VChestKey
  fromVal (VChestKey x) = x

instance IsoValue TxRollupL2Address where
  type ToT TxRollupL2Address = 'TTxRollupL2Address
  toVal = VTxRollupL2Address
  fromVal (VTxRollupL2Address 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 = (IsoValue a, WellTyped (ToT a))
type HasNoOpToT a = (IsoValue a, HasNoOp (ToT a))
type HasNoBigMapToT a = (IsoValue 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, HasNoNestedBigMaps (ToT 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)

type instance Index (BigMap k _) = k
type instance IxValue (BigMap _ v) = v
instance Ord k => Ixed (BigMap k v)
instance Ord k => At (BigMap k v) where
  at key handler (BigMap bmId bmMap) = BigMap bmId <$> at key handler bmMap

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 => ToBigMap (SizedList' n (k, v)) where
  type ToBigMapValue (SizedList' n (k, v)) = v
  type ToBigMapKey (SizedList' n (k, v)) = k
  mkBigMap = Exts.fromList . Prelude.toList

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 ToTs' :: forall k. [k] -> [T]
type family ToTs' 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