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

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

module Morley.Michelson.Typed.Value
  ( Comparability (..)
  , Comparable
  , ComparabilityScope
  , 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 Data.Singletons (Sing)
import Data.Type.Bool (type (&&))
import Fmt (Buildable(build), Builder, (+|), (|+))

import Morley.Michelson.Text (MText)
import Morley.Michelson.Typed.Contract
import Morley.Michelson.Typed.Entrypoints
import Morley.Michelson.Typed.Scope
import Morley.Michelson.Typed.Sing
import Morley.Michelson.Typed.T (T(..))
import Morley.Tezos.Address (Address, GlobalCounter(..))
import Morley.Tezos.Core (ChainId, Mutez, Timestamp)
import Morley.Tezos.Crypto
  (Bls12381Fr, Bls12381G1, Bls12381G2, Chest, ChestKey, KeyHash, PublicKey, Signature)
import Morley.Util.Sing (eqParamMixed3, eqParamSing)
import Morley.Util.TH

-- | 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
    :: ( forall i o. Show (instr i o)
       , forall i o. NFData (instr i o)
       , 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) -> tt1 `eqParamSing` tt2
    (OpTransferTokens _, _) -> False
    (OpSetDelegate sd1, OpSetDelegate sd2) -> sd1 == sd2
    (OpSetDelegate _, _) -> False
    (OpCreateContract cc1, OpCreateContract cc2) -> cc1 `eqParamMixed3` cc2
    (OpCreateContract _, _) -> False

data TransferTokens instr p = TransferTokens
  { ttTransferArgument :: Value' instr p
  , ttAmount :: Mutez
  , ttContract :: Value' instr ('TContract p)
  , ttCounter :: GlobalCounter
  } 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
  , sdCounter :: GlobalCounter
  } 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
  = ( forall i o. Show (instr i o)
    , forall i o. Eq (instr i o)
    )
  => CreateContract
  { ccOriginator :: Address
  , ccDelegate :: Maybe KeyHash
  , ccBalance :: Mutez
  , ccStorageVal :: Value' instr st
  , ccContract :: Contract' instr cp st
  , ccCounter :: GlobalCounter
  }

instance
  ( forall i o. NFData (instr i o)
  ) => NFData (CreateContract instr cp st) where
  rnf (CreateContract a b c d e f) = rnf (a, b, c, d, e, f)

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)

-- | Wrapper over instruction which remembers whether this instruction
-- always fails or not.
data RemFail (instr :: k -> k -> 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

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

instance (Comparable e1, Comparable e2, FailOnNonComparableFound (IsComparable e1 && IsComparable e2))
  => Comparable ('TPair e1 e2) where
  tcompare (VPair a) (VPair b) = compare a b
instance (Comparable e1, Comparable e2, FailOnNonComparableFound (IsComparable e1 && IsComparable e2))
  => Comparable ('TOr e1 e2) where
  tcompare (VOr a) (VOr b) = compare a b
instance (Comparable e, ForbidNonComparable e) => Comparable ('TOption e) where
  tcompare (VOption a) (VOption b) = compare a b
instance Comparable 'TUnit where
  tcompare VUnit VUnit = EQ
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 'TNever where
  tcompare = \case
instance Comparable 'TChainId where
  tcompare (VChainId a) (VChainId b) = compare a b
instance Comparable 'TSignature where
  tcompare (VSignature a) (VSignature b) = compare a b
instance Comparable 'TKey where
  tcompare (VKey a) (VKey b) = compare a b

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

-- | Alias for comparable types.
type ComparabilityScope t =
  (SingI 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
  STOr a b -> case (checkComparability a, checkComparability b) of
    (CanBeCompared, CanBeCompared) -> CanBeCompared
    (CannotBeCompared, _) -> CannotBeCompared
    (_, CannotBeCompared) -> CannotBeCompared
  STOption t -> case checkComparability t of
    CanBeCompared -> CanBeCompared
    CannotBeCompared -> CannotBeCompared
  STList _ -> CannotBeCompared
  STSet _ -> CannotBeCompared
  STOperation -> CannotBeCompared
  STContract _ -> CannotBeCompared
  STTicket _ -> CannotBeCompared
  STLambda _ _ -> CannotBeCompared
  STMap _ _ -> CannotBeCompared
  STBigMap _ _ -> CannotBeCompared
  STChest -> CannotBeCompared
  STChestKey -> CannotBeCompared
  STNever -> CanBeCompared
  STUnit -> CanBeCompared
  STInt -> CanBeCompared
  STNat -> CanBeCompared
  STString -> CanBeCompared
  STBytes -> CanBeCompared
  STMutez -> CanBeCompared
  STBool -> CanBeCompared
  STKeyHash -> CanBeCompared
  STBls12381Fr -> CannotBeCompared
  STBls12381G1 -> CannotBeCompared
  STBls12381G2 -> CannotBeCompared
  STTimestamp -> CanBeCompared
  STAddress -> CanBeCompared
  STKey -> CanBeCompared
  STSignature -> CanBeCompared
  STChainId -> 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 (SingI 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.
       (SingI t)
    => Maybe (Value' instr t) -> Value' instr ('TOption t)
  VList
    :: forall t instr.
       (SingI t)
    => [Value' instr t] -> Value' instr ('TList t)
  VSet
    :: forall t instr.
       (SingI t, Comparable t)
    => Set (Value' instr t) -> Value' instr ('TSet t)
  VOp
    :: Operation' instr -> Value' instr 'TOperation
  VContract
    :: forall arg instr.
       (SingI arg, HasNoOp arg)
    => Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
  VTicket
    :: forall arg instr.
       (Comparable arg)
    => Address -> Value' instr arg -> Natural -> Value' instr ('TTicket arg)
  VPair
    :: forall l r instr.
       (Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
  VOr
    :: forall l r instr.
       (SingI l, SingI r)
    => Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
  VLam
    :: forall inp out instr.
       ( SingI inp, SingI 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.
       (SingI k, SingI v, Comparable k)
    => Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
  VBigMap
    :: forall k v instr.
       (SingI k, SingI v, Comparable k, HasNoBigMap v)
    => Maybe Natural -- ^ The big_map's ID. This is only used in the interpreter.
    -> 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
  VBls12381Fr :: Bls12381Fr -> Value' instr 'TBls12381Fr
  VBls12381G1 :: Bls12381G1 -> Value' instr 'TBls12381G1
  VBls12381G2 :: Bls12381G2 -> Value' instr 'TBls12381G2
  VChest      :: Chest -> Value' instr 'TChest
  VChestKey   :: ChestKey -> Value' instr 'TChestKey

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 |+ ""

-- | Turn 'EpLiftSequence' into actual function on t'Morley.Michelson.Typed.Aliases.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 (SingI t)
valueTypeSanity = \case
  VKey{} -> Dict
  VUnit{} -> Dict
  VSignature{} -> Dict
  VChainId{} -> Dict
  VOption{} -> Dict
  VList{} -> Dict
  VSet{} -> Dict
  VOp{} -> Dict
  VContract _ (SomeEpc EntrypointCall{}) -> Dict
  VTicket _ v _ -> case valueTypeSanity v of
    Dict -> 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
  VBls12381Fr{} -> Dict
  VBls12381G1{} -> Dict
  VBls12381G2{} -> Dict
  VTimestamp{} -> Dict
  VAddress{} -> Dict
  VChest{} -> Dict
  VChestKey{} -> Dict

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

-- | Extended values comparison - it does not require t'Morley.Michelson.Typed.Aliases.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 `eqParamSing` 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')