{-# LANGUAGE QuantifiedConstraints #-}

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

module Michelson.Typed.Value
  ( Value' (..)
  , SomeValue' (..)
  , SomeConstrainedValue' (..)
  , ContractInp1
  , ContractInp
  , ContractOut1
  , ContractOut
  , CreateContract (..)
  , CValue (..)
  , Operation' (..)
  , SetDelegate (..)
  , TransferTokens (..)
  , RemFail (..)
  , rfMerge
  , rfAnyInstr
  , rfMapAnyInstr
  , addressToVContract
  , buildVContract
  , compileEpLiftSequence
  ) where

import Data.Default (def)
import Data.Singletons (SingI)
import Fmt (Buildable(build), (+|), (|+), Builder)
import qualified Data.Kind as Kind

import Michelson.Typed.CValue (CValue(..))
import Michelson.Typed.EntryPoints
import Michelson.Typed.Scope (ParameterScope, StorageScope)
import Michelson.Typed.T (T(..))
import Tezos.Address (Address)
import Tezos.Core (ChainId, Mutez)
import Tezos.Crypto (KeyHash, PublicKey, Signature)
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))
       , 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 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 (Show, Eq)

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

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

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

deriving instance Show (CreateContract instr cp st)
deriving 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 instance (forall o'. Show (instr i o')) => Show (RemFail instr i o)

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

-- | 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
  VC :: CValue t -> Value' instr ('Tc t)
  VKey :: PublicKey -> Value' instr 'TKey
  VUnit :: Value' instr 'TUnit
  VSignature :: Signature -> Value' instr 'TSignature
  VChainId :: ChainId -> Value' instr 'TChainId
  VOption :: forall t instr. Maybe (Value' instr t) -> Value' instr ('TOption t)
  VList :: forall t instr. [Value' instr t] -> Value' instr ('TList t)
  VSet :: forall t instr. Set (CValue 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. Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
  VLam
    :: forall inp out instr.
       ( forall i o.
          ( Show (instr i o)
          , Eq (instr i o)
          )
       )
    => RemFail instr (inp ': '[]) (out ': '[]) -> Value' instr ('TLambda inp out)
  VMap :: forall k v instr. Map (CValue k) (Value' instr v) -> Value' instr ('TMap k v)
  VBigMap :: forall k v instr. Map (CValue k) (Value' instr v) -> Value' instr ('TBigMap k v)

deriving instance Show (Value' instr t)
deriving 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
  => Address -> Value' instr ('TContract t)
addressToVContract addr = VContract addr def

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

data SomeValue' instr where
  SomeValue :: (Typeable t, SingI t) => Value' instr t -> SomeValue' instr

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

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