{-# LANGUAGE DerivingStrategies #-}

-- | Conversions between haskell types/values and Michelson ones.
module Michelson.Typed.Haskell.Value
  ( -- * Value conversions
    IsoCValue (..)
  , IsoValue (..)
  , GIsoValue (GValueType)
  , ToT'
  , SomeIsoValue (..)
  , AnyIsoValue (..)
  , IsComparable
  , IsGenericIsoValue

    -- * Missing Haskell analogies to Michelson values
  , EntryPointCall
  , SomeEntryPointCall
  , ContractRef (..)
  , coerceContractRef
  , BigMap (..)

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

import Data.Default (Default (..))
import qualified Data.Kind as Kind
import Data.Constraint (Dict (..), (:-)(..))
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.CValue
import Michelson.Typed.EntryPoints
import Michelson.Typed.T
import Michelson.Typed.Value
import Tezos.Address (Address)
import Tezos.Core (Mutez, Timestamp, ChainId)
import Tezos.Crypto (KeyHash, PublicKey, Signature)
import Util.Type

----------------------------------------------------------------------------
-- Comparable values isomorphism
----------------------------------------------------------------------------

-- | Isomorphism between Michelson primitive values and plain Haskell types.
class IsoCValue a where
  -- | Type function that converts a regular Haskell type into a comparable type
  -- (which has kind @CT@).
  type ToCT a :: CT

  -- | Converts a single Haskell value into @CVal@ representation.
  toCVal :: a -> CValue (ToCT a)

  -- | Converts a @CVal@ value into a single Haskell value.
  fromCVal :: CValue (ToCT a) -> a

instance IsoCValue Integer where
  type ToCT Integer = 'CInt
  toCVal = CvInt
  fromCVal (CvInt i) = i

instance IsoCValue Natural where
  type ToCT Natural = 'CNat
  toCVal = CvNat
  fromCVal (CvNat i) = i

instance IsoCValue MText where
  type ToCT MText = 'CString
  toCVal = CvString
  fromCVal (CvString s) = s

instance DoNotUseTextError => IsoCValue Text where
  type ToCT Text = DoNotUseTextError
  toCVal = error "impossible"
  fromCVal _ = error "impossible"

instance IsoCValue Bool where
  type ToCT Bool = 'CBool
  toCVal = CvBool
  fromCVal (CvBool b) = b

instance IsoCValue ByteString where
  type ToCT ByteString = 'CBytes
  toCVal = CvBytes
  fromCVal (CvBytes b) = b

instance IsoCValue Mutez where
  type ToCT Mutez = 'CMutez
  toCVal = CvMutez
  fromCVal (CvMutez m) = m

-- | This instance erases reference to contract entrypoint!
-- If this is an issue, use `EpAddress` instead.
--
-- Applications which use addresses just as participants identifiers
-- should not experience problems with using plain 'Address'.
instance IsoCValue Address where
  type ToCT Address = 'CAddress
  toCVal addr = CvAddress $ EpAddress addr def
  fromCVal (CvAddress a) = eaAddress a

instance IsoCValue EpAddress where
  type ToCT EpAddress = 'CAddress
  toCVal = CvAddress
  fromCVal (CvAddress a) = a

instance IsoCValue KeyHash where
  type ToCT KeyHash = 'CKeyHash
  toCVal = CvKeyHash
  fromCVal (CvKeyHash k) = k

instance IsoCValue Timestamp where
  type ToCT Timestamp = 'CTimestamp
  toCVal = CvTimestamp
  fromCVal (CvTimestamp t) = t

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

-- | Isomorphism between Michelson values and plain Haskell types.
--
-- Default implementation of this typeclass converts ADTs to Michelson
-- "pair"s and "or"s.
class 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 :: (Typeable a, IsoValue a) => a -> SomeIsoValue

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

-- | A useful property which holds for all 'CT' types.
type IsComparable c = ToT c ~ 'Tc (ToCT c)

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

instance IsoValue Integer where
  type ToT Integer = 'Tc (ToCT Integer)
  toVal = VC . toCVal
  fromVal (VC x) = fromCVal x

instance IsoValue Natural where
  type ToT Natural = 'Tc (ToCT Natural)
  toVal = VC . toCVal
  fromVal (VC x) = fromCVal x

instance IsoValue MText where
  type ToT MText = 'Tc (ToCT MText)
  toVal = VC . toCVal
  fromVal (VC x) = fromCVal x

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

instance IsoValue Bool where
  type ToT Bool = 'Tc (ToCT Bool)
  toVal = VC . toCVal
  fromVal (VC x) = fromCVal x

instance IsoValue ByteString where
  type ToT ByteString = 'Tc (ToCT ByteString)
  toVal = VC . toCVal
  fromVal (VC x) = fromCVal x

instance IsoValue Mutez where
  type ToT Mutez = 'Tc (ToCT Mutez)
  toVal = VC . toCVal
  fromVal (VC x) = fromCVal x

instance IsoValue KeyHash where
  type ToT KeyHash = 'Tc (ToCT KeyHash)
  toVal = VC . toCVal
  fromVal (VC x) = fromCVal x

instance IsoValue Timestamp where
  type ToT Timestamp = 'Tc (ToCT Timestamp)
  toVal = VC . toCVal
  fromVal (VC x) = fromCVal x

instance IsoValue Address where
  type ToT Address = 'Tc (ToCT Address)
  toVal = VC . toCVal
  fromVal (VC x) = fromCVal x

instance IsoValue EpAddress where
  type ToT EpAddress = 'Tc (ToCT EpAddress)
  toVal = VC . toCVal
  fromVal (VC x) = fromCVal 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 (Ord c, IsoCValue c) => IsoValue (Set c) where
  type ToT (Set c) = 'TSet (ToCT c)
  toVal = VSet . Set.map toCVal
  fromVal (VSet x) = Set.map fromCVal x

instance (Ord k, IsoCValue k, IsoValue v) => IsoValue (Map k v) where
  type ToT (Map k v) = 'TMap (ToCT k) (ToT v)
  toVal = VMap . Map.mapKeys toCVal . Map.map toVal
  fromVal (VMap x) = Map.map fromVal $ Map.mapKeys fromCVal 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)

-- | Since @Contract@ name is used to designate contract code, lets call
-- analogy of 'TContract' type as follows.
data ContractRef (arg :: Kind.Type) = ContractRef
  { crAddress :: Address
  , crEntryPoint :: SomeEntryPointCall arg
  } deriving stock (Eq, Show)

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

instance 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{..}

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

instance (Ord k, IsoCValue k, IsoValue v) => IsoValue (BigMap k v) where
  type ToT (BigMap k v) = 'TBigMap (ToCT k) (ToT v)
  toVal = VBigMap . Map.mapKeys toCVal . Map.map toVal . unBigMap
  fromVal (VBigMap x) = BigMap $ Map.map fromVal $ Map.mapKeys fromCVal 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.
class 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 IsGenericIsoValue 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