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

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

module Morley.Michelson.Typed.Value
  ( Comparability (..)
  , CreateContract (..)
  , Operation' (..)
  , SetDelegate (..)
  , TransferTokens (..)
  , Emit(..)
  , Value' (..)
  , RemFail (..)
  , LambdaCode' (..)
  , mkVLam
  , mkVLamRec
  , rfMerge
  , rfAnyInstr
  , rfMapAnyInstr
  , addressToVContract
  , buildVContract
  , checkComparability
  , compileEpLiftSequence
  , liftCallArg
  , valueTypeSanity
  , withValueTypeSanity
  , eqValueExt
  ) where

import Control.Lens (At(..), Index, IxValue, Ixed(..))
import Data.Constraint (Dict(..), (\\))
import Data.GADT.Compare (GEq(..))
import Fmt (Buildable(build), Doc, (+|), (|+))

import Morley.Michelson.Text (MText)
import Morley.Michelson.Typed.Annotation (Notes)
import Morley.Michelson.Typed.Contract
import Morley.Michelson.Typed.Entrypoints
import Morley.Michelson.Typed.Scope
import Morley.Michelson.Typed.T (T(..))
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.Sing (eqParamMixed3, eqParamSing, geqI)
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
  OpEmit :: PackedValScope t => Emit instr t -> Operation' instr

instance (forall t. Buildable (Value' instr t)) => Buildable (Operation' instr) where
  build =
    \case
      OpTransferTokens tt -> build tt
      OpSetDelegate sd -> build sd
      OpCreateContract cc -> build cc
      OpEmit em -> build em

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
    (OpEmit em1, OpEmit em2) -> em1 `eqParamSing` em2
    (OpEmit _, _) -> 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 Buildable (Value' instr p) => Buildable (TransferTokens instr p) where
  build TransferTokens {..} =
    "Transfer " +| ttAmount |+ " tokens to " +| buildVContract ttContract |+
      " with parameter " +| ttTransferArgument |+ ""

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 :: L1Address
  , ccDelegate :: Maybe KeyHash
  , ccBalance :: Mutez
  , ccStorageVal :: Value' instr st
  , ccContract :: Contract' instr cp st
  , ccCounter :: GlobalCounter
  }

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

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

data Emit instr t = PackedValScope t => Emit
  { emTag :: Text
  , emNotes :: Notes t
  , emValue :: Value' instr t
  , emCounter :: GlobalCounter
  }

deriving stock instance Show (Emit instr t)
deriving stock instance Eq (Emit instr t)

instance Buildable (Value' instr t) => Buildable (Emit instr t) where
  build Emit{..} = "Emit contract event with tag " +| emTag |+ ", type " +| emNotes |+
    " and payload " +| emValue |+ ""

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

tcompare :: forall t instr. Comparable t => (Value' instr t) -> (Value' instr t) -> Ordering
tcompare (VPair a) (VPair b) = compare a b
tcompare (VOr a) (VOr b) = compare a b
tcompare (VOption a) (VOption b) = compare a b
tcompare VUnit VUnit = EQ
tcompare (VInt a) (VInt b) = compare a b
tcompare (VNat a) (VNat b) = compare a b
tcompare (VString a) (VString b) = compare a b
tcompare (VBytes a) (VBytes b) = compare a b
tcompare (VMutez a) (VMutez b) = compare a b
tcompare (VBool a) (VBool b) = compare a b
tcompare (VKeyHash a) (VKeyHash b) = compare a b
tcompare (VTimestamp a) (VTimestamp b) = compare a b
tcompare (VAddress a) (VAddress b) = compare a b
tcompare (VChainId a) (VChainId b) = compare a b
tcompare (VSignature a) (VSignature b) = compare a b
tcompare (VKey a) (VKey b) = compare a b

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

{- | Representation of a Michelson value.

Since values (i.e. lambdas, operations) can include instructions, this type
depends on the type used to represent instructions, which is the parameter
@instr@. It is itself a polymorphic type, parametrized by the Michelson types of
its input and output stacks.

The primary motivator for polymorphism is breaking cyclic dependencies between
this module and "Morley.Michelson.Typed.Instr". In principle @instr@ can also be
used as an extension point, but at the time of writing it isn't used as such, it
is always eventually unified with @Instr@.

@t@ is the value's Michelson type.
-}
type Value' :: ([T] -> [T] -> Type) -> T -> Type
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.
       Comparable t
    => Set (Value' instr t) -> Value' instr ('TSet t)
  VOp
    :: Operation' instr -> Value' instr 'TOperation
  VContract
    :: forall arg instr.
       (SingI arg, ForbidOp 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)
    => LambdaCode' instr inp out
    -> Value' instr ('TLambda inp out)
  VMap
    :: forall k v instr.
       (SingI v, Comparable k)
    => Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
  VBigMap
    :: forall k v instr.
       (SingI v, Comparable k, ForbidBigMap 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)

{- | Code of a lambda value, either recursive or non-recursive.

Note the quantified constraints on the constructors. We opt to carry those here
and not on the respective instances for the sake of simplifying downstream
instance definitions. Constraining each instance with quantified constraints
gets very long-winded very fast, and it wouldn't work with 'deriveGADTNFData'.
-}
data LambdaCode' instr inp out where
  LambdaCode
    :: ( 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 ': '[])
    -> LambdaCode' instr inp out
  LambdaCodeRec
    :: ( forall i o. Show (instr i o)
       , forall i o. Eq (instr i o)
       , forall i o. NFData (instr i o))
    => RemFail instr (inp ': 'TLambda inp out ': '[]) (out ': '[])
    -> LambdaCode' instr inp out

deriving stock instance Show (LambdaCode' instr inp out)
deriving stock instance Eq (LambdaCode' instr inp out)

instance GEq (Value' instr) where
  geq l r = geqI l r \\ valueTypeSanity l \\ valueTypeSanity r

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

buildVContract :: Value' instr ('TContract arg) -> Doc
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

mkVLam
  :: ( 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)
     )
  => (IsNotInView => RemFail instr '[inp] '[out])
  -> Value' instr ('TLambda inp out)
mkVLam rf = VLam . LambdaCode $ giveNotInView rf

mkVLamRec
  :: ( 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)
     )
  => (IsNotInView => RemFail instr '[inp, 'TLambda inp out] '[out])
  -> Value' instr ('TLambda inp out)
mkVLamRec rf = VLam . LambdaCodeRec $ giveNotInView rf

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

mconcat [[d|
  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)
  |]
  , deriveGADTNFData ''Operation'
  , deriveGADTNFData ''Value'
  , deriveGADTNFData ''LambdaCode'
  ]

instance NFData (Emit instr t) where
  rnf (Emit a b c d) =
    rnf a `seq` rnf b `seq` rnf c `seq` rnf d

instance NFData (TransferTokens instr p)

type instance Index (Value' _ ('TList _)) = Int
type instance IxValue (Value' instr ('TList elem)) = Value' instr elem
instance Ixed (Value' instr ('TList elem)) where
  ix idx handler (VList xs) = VList <$> ix idx handler xs

type instance Index (Value' instr ('TMap k _)) = Value' instr k
type instance IxValue (Value' instr ('TMap _ v)) = Value' instr v
instance Ixed (Value' instr ('TMap k v))
instance At (Value' instr ('TMap k v)) where
  at key handler (VMap vmap) = VMap <$> at key handler vmap

type instance Index (Value' instr ('TBigMap k _)) = Value' instr k
type instance IxValue (Value' instr ('TBigMap _ v)) = Value' instr v
instance Ixed (Value' instr ('TBigMap k v))
instance At (Value' instr ('TBigMap k v)) where
  at key handler (VBigMap bmid bmap) = VBigMap bmid <$> at key handler bmap

type instance Index (Value' instr ('TSet a)) = Value' instr a
type instance IxValue (Value' _ ('TSet _)) = ()
instance Ixed (Value' instr ('TSet a))
instance At (Value' instr ('TSet a)) where
  at key handler (VSet vset) = VSet <$> at key handler vset