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

{-# LANGUAGE QuantifiedConstraints #-}

-- | Module, containing data types for Michelson value.

module Michelson.Typed.Value
  ( SomeValue' (..)
  , SomeConstrainedValue' (..)
  , Comparability (..)
  , Comparable
  , ComparabilityScope
  , ContractInp1
  , ContractInp
  , ContractOut1
  , ContractOut
  , CreateContract (..)
  , Operation' (..)
  , SetDelegate (..)
  , TransferTokens (..)
  , Value' (..)
  , RemFail (..)
  , rfMerge
  , rfAnyInstr
  , rfMapAnyInstr
  , addressToVContract
  , buildVContract
  , checkComparability
  , compileEpLiftSequence
  , comparabilityPresence
  , getComparableProofS
  , liftCallArg
  , valueTypeSanity
  , withValueTypeSanity
  , eqValueExt
  ) where

import Data.Constraint (Dict(..), (\\))
import qualified Data.Kind as Kind
import Data.Singletons (Sing, SingI(..))
import Data.Type.Bool (type (&&))
import Fmt (Buildable(build), Builder, (+|), (|+))
import GHC.TypeLits (ErrorMessage(..), TypeError)

import Michelson.Text (MText)
import Michelson.Typed.Entrypoints
import Michelson.Typed.Scope (BadTypeForScope(..), CheckScope(..), ParameterScope, StorageScope)
import Michelson.Typed.Sing
import Michelson.Typed.T (T(..))
import Tezos.Address (Address)
import Tezos.Core (ChainId, Mutez, Timestamp)
import Tezos.Crypto (KeyHash, PublicKey, Signature)
import Util.TH
import Util.Typeable

-- | Data type, representing operation, list of which is returned
-- by Michelson contract (according to calling convention).
--
-- These operations are to be further executed against system state
-- after the contract execution.
data Operation' instr where
  OpTransferTokens
    :: (ParameterScope p)
    => TransferTokens instr p -> Operation' instr
  OpSetDelegate :: SetDelegate -> Operation' instr
  OpCreateContract
    :: ( Show (instr (ContractInp cp st) (ContractOut st))
       , NFData (instr (ContractInp cp st) (ContractOut st))
       , Typeable instr, ParameterScope cp, StorageScope st)
    => CreateContract instr cp st
    -> Operation' instr

instance Buildable (Operation' instr) where
  build =
    \case
      OpTransferTokens tt -> build tt
      OpSetDelegate sd -> build sd
      OpCreateContract cc -> build cc

deriving stock instance Show (Operation' instr)

instance Eq (Operation' instr) where
  op1 == op2 = case (op1, op2) of
    (OpTransferTokens tt1, OpTransferTokens tt2) -> eqParam1 tt1 tt2
    (OpTransferTokens _, _) -> False
    (OpSetDelegate sd1, OpSetDelegate sd2) -> sd1 == sd2
    (OpSetDelegate _, _) -> False
    (OpCreateContract cc1, OpCreateContract cc2) -> eqParam3 cc1 cc2
    (OpCreateContract _, _) -> False

data TransferTokens instr p = TransferTokens
  { ttTransferArgument :: Value' instr p
  , ttAmount :: Mutez
  , ttContract :: Value' instr ('TContract p)
  } deriving stock (Show, Eq, Generic)

instance NFData (TransferTokens instr p)

instance Buildable (TransferTokens instr p) where
  build TransferTokens {..} =
    "Transfer " +| ttAmount |+ " tokens to " +| buildVContract ttContract |+ ""

data SetDelegate = SetDelegate
  { sdMbKeyHash :: Maybe KeyHash
  } deriving stock (Show, Eq, Generic)

instance NFData SetDelegate

instance Buildable SetDelegate where
  build (SetDelegate mbDelegate) =
    "Set delegate to " <> maybe "<nobody>" build mbDelegate

data CreateContract instr cp st
  = ( Show (instr (ContractInp cp st) (ContractOut st))
    , Eq (instr (ContractInp cp st) (ContractOut st))
    )
  => CreateContract
  { ccOriginator :: Address
  , ccDelegate :: Maybe KeyHash
  , ccBalance :: Mutez
  , ccStorageVal :: Value' instr st
  , ccContractCode :: instr (ContractInp cp st) (ContractOut st)
  }

instance NFData (instr (ContractInp cp st) (ContractOut st)) => NFData (CreateContract instr cp st) where
  rnf (CreateContract a b c d e) = rnf (a, b, c, d, e)

instance Buildable (CreateContract instr cp st) where
  build CreateContract {..} =
    "Create a new contract with" <>
    " delegate " +| maybe "<nobody>" build ccDelegate |+
    " and balance = " +| ccBalance |+ ""

deriving stock instance Show (CreateContract instr cp st)
deriving stock instance Eq (CreateContract instr cp st)

type ContractInp1 param st = 'TPair param st
type ContractInp param st = '[ ContractInp1 param st ]

type ContractOut1 st = 'TPair ('TList 'TOperation) st
type ContractOut st = '[ ContractOut1 st ]

-- | Wrapper over instruction which remembers whether this instruction
-- always fails or not.
data RemFail (instr :: k -> k -> Kind.Type) (i :: k) (o :: k) where
  RfNormal :: instr i o -> RemFail instr i o
  RfAlwaysFails :: (forall o'. instr i o') -> RemFail instr i o

deriving stock instance (forall o'. Show (instr i o')) => Show (RemFail instr i o)
instance (forall o'. NFData (instr i o')) => NFData (RemFail instr i o) where
  rnf (RfNormal a) = rnf a
  rnf (RfAlwaysFails a) = rnf a

-- | Ignoring distinction between constructors here, comparing only semantics.
instance Eq (instr i o) => Eq (RemFail instr i o) where
  RfNormal i1 == RfNormal i2 = i1 == i2
  RfAlwaysFails i1 == RfNormal i2 = i1 == i2
  RfNormal i1 == RfAlwaysFails i2 = i1 == i2
  RfAlwaysFails i1 == RfAlwaysFails i2 = i1 @o == i2

-- | Merge two execution branches.
rfMerge
  :: (forall o'. instr i1 o' -> instr i2 o' -> instr i3 o')
  -> RemFail instr i1 o -> RemFail instr i2 o -> RemFail instr i3 o
rfMerge merger instr1 instr2 = case (instr1, instr2) of
  (RfNormal i1, RfNormal i2) -> RfNormal (merger i1 i2)
  (RfAlwaysFails i1, RfNormal i2) -> RfNormal (merger i1 i2)
  (RfNormal i1, RfAlwaysFails i2) -> RfNormal (merger i1 i2)
  (RfAlwaysFails i1, RfAlwaysFails i2) -> RfAlwaysFails (merger i1 i2)

-- | Get code disregard whether it always fails or not.
rfAnyInstr :: RemFail instr i o -> instr i o
rfAnyInstr = \case
  RfNormal i -> i
  RfAlwaysFails i -> i

-- | Modify inner code.
rfMapAnyInstr
  :: (forall o'. instr i1 o' -> instr i2 o')
  -> RemFail instr i1 o
  -> RemFail instr i2 o
rfMapAnyInstr f = \case
  RfNormal i -> RfNormal $ f i
  RfAlwaysFails i -> RfAlwaysFails $ f i

getComparableProofS :: Sing (a :: T) -> Maybe (Dict (Comparable a))
getComparableProofS s = case checkComparability s of
  CanBeCompared -> Just Dict
  CannotBeCompared -> Nothing

-- | Constraint which ensures that type is comparable.
type family IsComparable (t :: T) :: Bool where
  IsComparable ('TPair a b) =  IsComparable a && IsComparable b
  IsComparable 'TKey = 'False
  IsComparable 'TUnit = 'False
  IsComparable 'TSignature = 'False
  IsComparable 'TChainId = 'False
  IsComparable ('TOption _) = 'False
  IsComparable ('TList _) = 'False
  IsComparable ('TSet _) = 'False
  IsComparable 'TOperation = 'False
  IsComparable ('TContract _) = 'False
  IsComparable ('TOr _ _) = 'False
  IsComparable ('TLambda _ _) = 'False
  IsComparable ('TMap _ _) = 'False
  IsComparable ('TBigMap _ _) = 'False
  IsComparable _            = 'True

class (IsComparable t ~ 'True) => Comparable t where
  tcompare :: (Value' instr t) -> (Value' instr t) -> Ordering

instance (Comparable e1, Comparable e2) => Comparable ('TPair e1 e2) where
  tcompare (VPair a) (VPair b) = compare a b
instance Comparable 'TInt where
  tcompare (VInt a) (VInt b) = compare a b
instance Comparable 'TNat where
  tcompare (VNat a) (VNat b) = compare a b
instance Comparable 'TString where
  tcompare (VString a) (VString b) = compare a b
instance Comparable 'TBytes where
  tcompare (VBytes a) (VBytes b) = compare a b
instance Comparable 'TMutez where
  tcompare (VMutez a) (VMutez b) = compare a b
instance Comparable 'TBool where
  tcompare (VBool a) (VBool b) = compare a b
instance Comparable 'TKeyHash where
  tcompare (VKeyHash a) (VKeyHash b) = compare a b
instance Comparable 'TTimestamp where
  tcompare (VTimestamp a) (VTimestamp b) = compare a b
instance Comparable 'TAddress where
  tcompare (VAddress a) (VAddress b) = compare a b

instance (Comparable e) => Ord (Value' instr e) where
  compare = tcompare @e

-- | Report a human-readable error that 'TBigMap' contains another 'TBigMap'
type family FailOnNonComparable (isComparable :: Bool) :: Constraint where
  FailOnNonComparable 'False =
    TypeError ('Text "The type is not comparable")
  FailOnNonComparable 'True = ()

-- | Alias for comparable types.
type ComparabilityScope t =
  (KnownT t, Comparable t)

data Comparability t where
  CanBeCompared :: (Comparable t) => Comparability t
  CannotBeCompared :: (IsComparable t ~ 'False) => Comparability t

checkComparability :: Sing t -> Comparability t
checkComparability = \case
  STPair a b -> case (checkComparability a, checkComparability b) of
    (CanBeCompared, CanBeCompared) -> CanBeCompared
    (CannotBeCompared, _) -> CannotBeCompared
    (_, CannotBeCompared) -> CannotBeCompared
  STKey -> CannotBeCompared
  STUnit -> CannotBeCompared
  STSignature -> CannotBeCompared
  STChainId -> CannotBeCompared
  STOption _ -> CannotBeCompared
  STList _ -> CannotBeCompared
  STSet _ -> CannotBeCompared
  STOperation -> CannotBeCompared
  STContract _ -> CannotBeCompared
  STOr _ _ -> CannotBeCompared
  STLambda _ _ -> CannotBeCompared
  STMap _ _ -> CannotBeCompared
  STBigMap _ _ -> CannotBeCompared
  STInt -> CanBeCompared
  STNat -> CanBeCompared
  STString -> CanBeCompared
  STBytes -> CanBeCompared
  STMutez -> CanBeCompared
  STBool -> CanBeCompared
  STKeyHash -> CanBeCompared
  STTimestamp -> CanBeCompared
  STAddress -> CanBeCompared

comparabilityPresence :: Sing t -> Maybe (Dict $ (Comparable t))
comparabilityPresence s = case checkComparability s of
  CanBeCompared -> Just Dict
  CannotBeCompared -> Nothing

instance SingI t => CheckScope (Comparable t) where
  checkScope = maybeToRight BtNotComparable $ comparabilityPresence sing

instance (KnownT t) => CheckScope (ComparabilityScope t) where
  checkScope =
    (\Dict -> Dict) <$> checkScope @(Comparable t)

-- | Representation of Michelson value.
--
-- Type parameter @instr@ stands for Michelson instruction
-- type, i.e. data type to represent an instruction of language.

data Value' instr t where
  VKey :: PublicKey -> Value' instr 'TKey
  VUnit :: Value' instr 'TUnit
  VSignature :: Signature -> Value' instr 'TSignature
  VChainId :: ChainId -> Value' instr 'TChainId
  VOption
    :: forall t instr.
       (KnownT t)
    => Maybe (Value' instr t) -> Value' instr ('TOption t)
  VList
    :: forall t instr.
       (KnownT t)
    => [Value' instr t] -> Value' instr ('TList t)
  VSet
    :: forall t instr.
       (KnownT t, Comparable t)
    => Set (Value' instr t) -> Value' instr ('TSet t)
  VOp
    :: Operation' instr -> Value' instr 'TOperation
  VContract
    :: forall arg instr.
       Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
  VPair
    :: forall l r instr.
       (Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
  VOr
    :: forall l r instr.
       (KnownT l, KnownT r)
    => Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
  VLam
    :: forall inp out instr.
       ( KnownT inp, KnownT out
       , forall i o. Show (instr i o)
       , forall i o. Eq (instr i o)
       , forall i o. NFData (instr i o)
       )
    => RemFail instr (inp ': '[]) (out ': '[]) -> Value' instr ('TLambda inp out)
  VMap
    :: forall k v instr.
       (KnownT k, KnownT v, Comparable k)
    => Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
  VBigMap
    :: forall k v instr.
       (KnownT k, KnownT v, Comparable k)
    => Map (Value' instr k) (Value' instr v) -> Value' instr ('TBigMap k v)
  VInt       :: Integer ->  Value' instr 'TInt
  VNat       :: Natural -> Value' instr 'TNat
  VString    :: MText -> Value' instr 'TString
  VBytes     :: ByteString -> Value' instr 'TBytes
  VMutez     :: Mutez -> Value' instr 'TMutez
  VBool      :: Bool -> Value' instr 'TBool
  VKeyHash   :: KeyHash -> Value' instr 'TKeyHash
  VTimestamp :: Timestamp -> Value' instr 'TTimestamp
  VAddress   :: EpAddress -> Value' instr 'TAddress

deriving stock instance Show (Value' instr t)
deriving stock instance Eq (Value' instr t)

-- | Make value of 'contract' type which refers to the given address and
-- does not call any entrypoint.
addressToVContract
  :: forall t instr.
      (ParameterScope t, ForbidOr t)
  => Address -> Value' instr ('TContract t)
addressToVContract addr = VContract addr sepcPrimitive

buildVContract :: Value' instr ('TContract arg) -> Builder
buildVContract = \case
  VContract addr epc -> "Contract " +| addr |+ " call " +| epc |+ ""

data SomeValue' instr where
  SomeValue :: KnownT t => Value' instr t -> SomeValue' instr

deriving stock instance Show (SomeValue' instr)

instance Eq (SomeValue' instr) where
  SomeValue v1 == SomeValue v2 = v1 `eqParam1` v2

data SomeConstrainedValue' instr (c :: T -> Constraint) where
  SomeConstrainedValue
    :: forall (t :: T) (c :: T -> Constraint) instr
    . (c t)
    => Value' instr t
    -> SomeConstrainedValue' instr c

deriving stock instance Show (SomeConstrainedValue' instr c)

-- TODO
-- @gromak: perhaps we should implement `SomeValue'` in terms of
-- `SomeConstrainedValue'`, but it will require changing quite a lot of code,
-- so it is postponed.

-- | Turn 'EpLiftSequence' into actual function on 'Value's.
compileEpLiftSequence
  :: EpLiftSequence arg param
  -> Value' instr arg
  -> Value' instr param
compileEpLiftSequence = \case
  EplArgHere -> id
  EplWrapLeft els -> VOr . Left . compileEpLiftSequence els
  EplWrapRight els -> VOr . Right . compileEpLiftSequence els

-- | Lift entrypoint argument to full parameter.
liftCallArg
  :: EntrypointCallT param arg
  -> Value' instr arg
  -> Value' instr param
liftCallArg epc = compileEpLiftSequence (epcLiftSequence epc)

-- | Get a witness of that value's type is known.
--
-- Note that we cannot pick such witness out of nowhere as not all types
-- of kind 'T' have 'Typeable' and 'SingI' instances; example:
--
-- @
-- type family Any :: T where
--   -- nothing here
-- @
valueTypeSanity :: Value' instr t -> Dict (KnownT t)
valueTypeSanity = \case
  VKey{} -> Dict
  VUnit{} -> Dict
  VSignature{} -> Dict
  VChainId{} -> Dict
  VOption{} -> Dict
  VList{} -> Dict
  VSet{} -> Dict
  VOp{} -> Dict
  VContract _ (SomeEpc EntrypointCall{}) -> Dict
  VPair (l, r) -> case (valueTypeSanity l, valueTypeSanity r) of
    (Dict, Dict) -> Dict
  VOr{} -> Dict
  VLam{} -> Dict
  VMap{} -> Dict
  VBigMap{} -> Dict
  VInt{} -> Dict
  VNat{} -> Dict
  VString{} -> Dict
  VBytes{} -> Dict
  VMutez{} -> Dict
  VBool{} -> Dict
  VKeyHash{} -> Dict
  VTimestamp{} -> Dict
  VAddress{} -> Dict

-- | Provide a witness of that value's type is known.
withValueTypeSanity :: Value' instr t -> (KnownT t => a) -> a
withValueTypeSanity v a = case valueTypeSanity v of Dict -> a

-- | Extended values comparison - it does not require 'Value's to be
-- of the same type, only their content to match.
eqValueExt :: Value' instr t1 -> Value' instr t2 -> Bool
eqValueExt v1 v2 =
  v1 `eqParam1` v2
    \\ valueTypeSanity v1
    \\ valueTypeSanity v2

-- TODO: actually we should handle big maps with something close
-- to following:
--
--  VBigMap :: BigMap op ref k v -> Value' cp ('TBigMap k v)
--
-- data Value'Op v
--     = New v
--     | Upd v
--     | Rem
--     | NotExisted
--
-- data BigMap op ref k v = BigMap
--  { bmRef :: ref k v, bmChanges :: Map (CValue k) (Value'Op (Value' cp v)) }

$(deriveGADTNFData ''Operation')
$(deriveGADTNFData ''Value')