-- 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 (..)
  , Value' (..)
  , RemFail (..)
  , rfMerge
  , rfAnyInstr
  , rfMapAnyInstr
  , addressToVContract
  , buildVContract
  , checkComparability
  , compileEpLiftSequence
  , getComparableProofS
  , liftCallArg
  , valueTypeSanity
  , withValueTypeSanity
  , eqValueExt
  ) where

import Control.Lens (At(..), Index, IxValue, Ixed(..))
import Data.Constraint (Dict(..), (\\))
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.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

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

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