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

module Morley.Michelson.TypeCheck.Value
    ( typeCheckValImpl
    , tcFailedOnValue
    ) where

import Control.Monad.Except (liftEither, throwError)
import Data.Constraint (Dict(..))
import Data.Default (def)
import qualified Data.List.NonEmpty as NE
import qualified Data.Map as M
import qualified Data.Set as S
import Data.Singletons (Sing, SingI(..), demote, fromSing, withSingI)
import Data.Typeable ((:~:)(..))
import Fmt (pretty)
import Prelude hiding (EQ, GT, LT)

import Morley.Michelson.Text
import Morley.Michelson.TypeCheck.Error (TCError(..), TCTypeError(..))
import Morley.Michelson.TypeCheck.Helpers
import Morley.Michelson.TypeCheck.TypeCheck
  (SomeParamType(..), TcInstrHandler, TcOriginatedContracts, TypeCheckInstr, TypeCheckOptions(..),
  throwingTCError)
import Morley.Michelson.TypeCheck.Types
import Morley.Michelson.Typed (EpAddress(..), Notes(..), SingT(..), Value'(..), starNotes)
import qualified Morley.Michelson.Typed as T
import qualified Morley.Michelson.Untyped as U
import Morley.Tezos.Address (Address(..))
import Morley.Tezos.Core
import Morley.Tezos.Crypto
import qualified Morley.Tezos.Crypto.BLS12381 as BLS
import Morley.Tezos.Crypto.Timelock (chestFromBytes, chestKeyFromBytes)
import Morley.Util.Type (onFirst)

tcFailedOnValue :: U.Value -> T.T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue v t msg err = do
  loc <- ask
  throwError $ TCFailedOnValue v t msg loc err

-- | Function @typeCheckValImpl@ converts a single Michelson value
-- given in representation from @Morley.Michelson.Type@ module to representation
-- in strictly typed GADT.
--
-- @typeCheckValImpl@ is polymorphic in the expected type of value.
--
-- Type checking algorithm pattern-matches on parse value representation,
-- expected type @t@ and constructs @Val t@ value.
--
-- If there was no match on a given pair of value and expected type,
-- that is interpreted as input of wrong type and type check finishes with
-- error.
--
-- @typeCheckValImpl@ also has a 'Maybe TcOriginatedContracts' argument that
-- should contain the originated contracts when typechecking a parameter and
-- 'Nothing' otherwise.
typeCheckValImpl
  :: forall ty.
     SingI ty
  => Maybe TcOriginatedContracts
  -> TcInstrHandler
  -> U.Value
  -> TypeCheckInstr (T.Value ty)
typeCheckValImpl mOriginatedContracts tcDo uv = doTypeCheckVal (uv, sing @ty)
  where
    doTypeCheckVal :: forall tz. (U.Value, Sing tz) -> TypeCheckInstr (T.Value tz)
    doTypeCheckVal (uvalue, sng) = case (uvalue, sng) of
      (U.ValueInt i, STInt) -> pure $ T.VInt i
      (v@(U.ValueInt i), t@STNat)
        | i >= 0 -> pure $ VNat (fromInteger i)
        | otherwise -> tcFailedOnValue v (fromSing t) "" (Just NegativeNat)
      (v@(U.ValueInt i), t@STMutez) -> case mkMutez i of
        Right m -> pure $ VMutez m
        Left err -> tcFailedOnValue v (fromSing t) err (Just InvalidTimestamp)
      (U.ValueString s, STString) -> pure $ VString s
      (v@(U.ValueString s), t@STAddress) -> case T.parseEpAddress (unMText s) of
        Right addr -> pure $ VAddress addr
        Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidAddress err)
      (v@(U.ValueBytes b), t@STAddress) -> case T.parseEpAddressRaw (U.unInternalByteString b) of
        Right addr -> pure $ VAddress addr
        Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidAddress err)
      (v@(U.ValueString s), t@STKeyHash) -> case parseKeyHash (unMText s)  of
        Right kHash -> pure $ VKeyHash kHash
        Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidKeyHash err)
      (v@(U.ValueBytes b), t@STKeyHash) ->
        case parseKeyHashRaw (U.unInternalByteString b) of
          Right kHash -> pure $ VKeyHash kHash
          Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidKeyHash err)
      (U.ValueInt i, STBls12381Fr) ->
        pure $ VBls12381Fr (fromIntegralOverflowing @Integer @Bls12381Fr i)
      (v@(U.ValueBytes b), t@STBls12381Fr) ->
        case BLS.fromMichelsonBytes (U.unInternalByteString b) of
          Right val -> pure $ VBls12381Fr val
          Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidBls12381Object err)
      (v@(U.ValueBytes b), t@STBls12381G1) ->
        case BLS.fromMichelsonBytes (U.unInternalByteString b) of
          Right val -> pure $ VBls12381G1 val
          Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidBls12381Object err)
      (v@(U.ValueBytes b), t@STBls12381G2) ->
        case BLS.fromMichelsonBytes (U.unInternalByteString b) of
          Right val -> pure $ VBls12381G2 val
          Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidBls12381Object err)
      (v@(U.ValueString s), t@STTimestamp) -> case parseTimestamp $ unMText s of
        Just tstamp -> pure $ VTimestamp tstamp
        Nothing -> tcFailedOnValue v (fromSing t) "" (Just InvalidTimestamp)
      (U.ValueInt i, STTimestamp) -> pure $ VTimestamp (timestampFromSeconds i)
      (U.ValueBytes (U.InternalByteString s), STBytes) -> pure $ VBytes s
      (U.ValueTrue, STBool) -> pure $ VBool True
      (U.ValueFalse, STBool) -> pure $ VBool False

      (U.ValueString (parsePublicKey . unMText -> Right s), STKey) ->
        pure $ T.VKey s
      (U.ValueBytes (parsePublicKeyRaw . U.unInternalByteString -> Right s), STKey) ->
        pure $ VKey s

      (U.ValueString (parseSignature . unMText -> Right s), STSignature) ->
        pure $ VSignature s
      (U.ValueBytes (parseSignatureRaw . U.unInternalByteString  -> Right s), STSignature) ->
        pure $ VSignature s

      (U.ValueString (parseChainId . unMText -> Right ci), STChainId) ->
        pure $ VChainId ci
      (U.ValueBytes (mkChainId . U.unInternalByteString -> Just ci), STChainId) ->
        pure $ VChainId ci

      (cv@(U.ValueString (T.parseEpAddress . unMText -> Right addr))
        , STContract pc) -> typecheckContractValue cv addr pc
      (cv@(U.ValueBytes (T.parseEpAddressRaw . U.unInternalByteString -> Right addr))
        , STContract pc) -> typecheckContractValue cv addr pc

      (cv, s@(STTicket vt)) -> lift (asks tcStrict) >>= \case
        -- Note [Tickets forging]
        -- Normally, ticket values cannot be constructed manually (i.e. forged)
        -- by design, and the only valid way to make a ticket is calling
        -- @TICKET@ instruction.
        --
        -- However @tezos-client run@ adds an exception, it allows passing a
        -- manually constructed ticket value as parameter or initial storage.
        True ->
          tcFailedOnValue cv (fromSing sng)
            "ticket values cannot be forged in real operations"
            Nothing
        False -> case cv of
          U.ValuePair addrV (U.ValuePair datV amV) -> withComparable vt cv s $ do
            addrValue <- doTypeCheckVal (addrV, STAddress)
            dat <- doTypeCheckVal (datV, vt)
            amountValue <- doTypeCheckVal (amV, STNat)
            case (addrValue, amountValue) of
              (VAddress (EpAddress addr ep), VNat am) -> do
                unless (U.isDefEpName ep) $
                  tcFailedOnValue cv (fromSing sng)
                    "it is pointless to provide an address with entrypoint as a \
                    \ticketer, we do not support that"
                    Nothing
                -- ↑ Tezos allows passing addresses with entrypoint, but it is
                -- not possible to sanely work with them after that anyway,
                -- since @TICKET@ instruction (the only valid way of constructing
                -- tickets in real run) uses @SELF_ADDRESS@ result as ticketer.
                return $ VTicket addr dat am
          _ ->
            tcFailedOnValue cv (fromSing sng)
              "ticket type expects a value of type `(pair address <data> nat)`"
              Nothing

      (U.ValueUnit, STUnit) -> pure $ VUnit
      (U.ValuePair ml mr, STPair lt rt) -> do
        l <- doTypeCheckVal (ml, lt)
        r <- doTypeCheckVal (mr, rt)
        pure $ VPair (l, r)
      (U.ValueLeft ml, STOr lt rt) -> do
        l <- doTypeCheckVal (ml, lt)
        withSingI lt $ withSingI rt $ pure $ VOr (Left l)
      (U.ValueRight mr, STOr lt rt) -> do
        r <- doTypeCheckVal (mr, rt)
        withSingI lt $ withSingI rt $ pure $ VOr (Right r)
      (U.ValueSome mv, STOption op) -> do
        v <- doTypeCheckVal (mv, op)
        withSingI op $ pure $ VOption (Just v)
      (U.ValueNone, STOption op) -> do
        withSingI op $ pure $ VOption Nothing

      (U.ValueNil, STList l) -> withSingI l $
        pure $ T.VList []

      -- If ValueSeq contains at least 2 elements, it can be type checked as a
      -- right combed pair.
      (U.ValueSeq vals@(_ :| (_ : _)), STPair _ _) ->
        doTypeCheckVal (seqToRightCombedPair vals, sng)

      (U.ValueSeq (toList -> mels), STList l) -> do
        els <- typeCheckValsImpl (mels, l)
        withSingI l $ pure $ VList els

      (U.ValueNil, STSet s) -> do
        instrPos <- ask
        case T.getComparableProofS s of
          Just Dict -> withSingI s $ pure (T.VSet S.empty)
          Nothing -> throwError $ TCFailedOnValue uvalue (fromSing s) "Non comparable types are not allowed in Sets"
            instrPos (Just $ UnsupportedTypeForScope (fromSing s) T.BtNotComparable)

      (sq@(U.ValueSeq (toList -> mels)), s@(STSet vt)) -> withComparable vt sq s $ do
        instrPos <- ask

        els <- typeCheckValsImpl (mels, vt)
        elsS <- liftEither $ S.fromDistinctAscList <$> ensureDistinctAsc id els
                  `onFirst` \msg -> TCFailedOnValue sq (fromSing vt) msg instrPos Nothing
        withSingI vt $ pure $ VSet elsS

      (v@U.ValueNil, s@(STMap st vt)) ->
        withSingI st $ withSingI vt $ withComparable st v s $ pure $ T.VMap M.empty

      (sq@(U.ValueMap (toList -> mels)), s@(STMap kt vt)) ->
        withComparable kt sq s $ do
          keyOrderedElts <- typeCheckMapVal mels sq kt vt
          withSingI kt $ withSingI vt $
            pure $ VMap (M.fromDistinctAscList keyOrderedElts)

      (v@U.ValueNil, s@(STBigMap st1 st2)) ->
        withSingI st1 $ withSingI st2 $ withComparable st1 v s $ withBigMapAbsence st2 v s $
          pure $ VBigMap Nothing M.empty

      (sq@(U.ValueMap (toList -> mels)), s@(STBigMap kt vt)) ->
        withComparable kt sq s $ withBigMapAbsence vt sq s $ do
          keyOrderedElts <- typeCheckMapVal mels sq kt vt
          withSingI kt $ withSingI vt $
            pure $ VBigMap Nothing (M.fromDistinctAscList keyOrderedElts)

      -- `{ {} }` can be typechecked either as `VLam` or `VList`.
      (U.ValueLambda s, STList l) ->
        case emptyLambdaAsList s of
          Just xs -> doTypeCheckVal (xs, sng)
          Nothing -> tcFailedOnValue uvalue (fromSing l) "" Nothing

      (U.ValueSeq s, STLambda _ _) -> case emptyListAsLambda s of
        Just xs -> doTypeCheckVal (xs, sng)
        Nothing -> tcFailedOnValue uvalue (fromSing sng) "" Nothing

      (v, STLambda (var :: Sing it) (b :: Sing ot)) -> withSingI var $ withSingI b $ do
        mp <- case v of
          U.ValueNil       -> pure []
          U.ValueLambda mp -> pure $ toList mp
          _ -> tcFailedOnValue v (demote @ty) "unexpected value" Nothing
        _ :/ instr <-
          withWTP @it uvalue $ throwingTCError $
            typeCheckImpl tcDo mp ((starNotes @it, Dict, def) ::& SNil)
        case instr of
          lam ::: (lo :: HST lo) -> withWTP @ot uvalue $ do
            case eqHST1 @ot lo of
              Right Refl -> do
                pure $ VLam (T.RfNormal lam)
              Left m ->
                tcFailedOnValue v (demote @ty)
                        "wrong output type of lambda's value:" (Just m)
          AnyOutInstr lam ->
            pure $ VLam (T.RfAlwaysFails lam)

      (v@(U.ValueBytes (U.InternalByteString bs)), STChest) ->
        case chestFromBytes bs of
          Right res -> pure $ VChest res
          Left err -> tcFailedOnValue v T.TChest err Nothing

      (v@(U.ValueBytes (U.InternalByteString bs)), STChestKey) ->
        case chestKeyFromBytes bs of
          Right res -> pure $ VChestKey res
          Left err -> tcFailedOnValue v T.TChestKey err Nothing

      (v, t) -> tcFailedOnValue v (fromSing t) "unknown value" Nothing

    seqToRightCombedPair :: (NonEmpty $ U.Value) -> U.Value
    seqToRightCombedPair (x :| [y]) = U.ValuePair x y
    seqToRightCombedPair (x :| xs) = U.ValuePair x $ seqToRightCombedPair (NE.fromList xs)

    -- Converts a lambda containing only empty 'SeqEx's (possibly nested)
    -- to a list of empty lists.
    emptyLambdaAsList :: NonEmpty U.ExpandedOp -> Maybe U.Value
    emptyLambdaAsList ops =
      let
        opToMaybeList :: U.ExpandedOp -> Maybe U.Value
        opToMaybeList = \case
          U.SeqEx []      -> Just U.ValueNil
          U.SeqEx xs      -> U.ValueSeq . NE.fromList <$> traverse opToMaybeList xs
          U.PrimEx {}     -> Nothing
          U.WithSrcEx _ i -> opToMaybeList i
      in
        U.ValueSeq <$> traverse opToMaybeList ops

    -- Converts a list containing only empty lists (possibly nested)
    -- to a lambda of empty 'SeqEx's.
    emptyListAsLambda :: NonEmpty U.Value -> Maybe U.Value
    emptyListAsLambda ops =
      let
        listToMaybeOp :: U.Value -> Maybe U.ExpandedOp
        listToMaybeOp = \case
          U.ValueNil      -> Just $ U.SeqEx []
          U.ValueSeq xs   -> U.SeqEx . toList <$> traverse listToMaybeOp xs
          _               -> Nothing
      in
        U.ValueLambda <$> traverse listToMaybeOp ops

    withWTP
      :: forall t a. SingI t
      => U.Value
      -> (T.WellTyped t => TypeCheckInstr a)
      -> TypeCheckInstr a
    withWTP uvalue fn = case getWTP @t of
      Right Dict -> fn
      Left (NotWellTyped t cause) -> tcFailedOnValue uvalue (demote @ty)
                  ("Value is not well typed: '" <> show t <> "' because it " <> pretty cause) Nothing

    typeCheckValsImpl
      :: ([U.Value], Sing t)
      -> TypeCheckInstr [T.Value t]
    typeCheckValsImpl (mvs, sng) =
      fmap reverse $ foldM (\res mv -> (: res) <$> (doTypeCheckVal (mv, sng))) [] mvs

    -- Typechecks given list of @Elt@s and ensures that its keys are in ascending order.
    --
    -- It return list of pairs (key, value) with keys in ascending order
    -- so it is safe to call @fromDistinctAscList@ on returned list
    typeCheckMapVal
      :: [U.Elt U.ExpandedOp]
      -> U.Value
      -> Sing kt
      -> Sing vt
      -> TypeCheckInstr [(T.Value kt, T.Value vt)]
    typeCheckMapVal mels sq kt vt = withComparable kt sq kt $ do
      instrPos <- ask
      ks <- typeCheckValsImpl (map (\(U.Elt k _) -> k) mels, kt)
      vals <- typeCheckValsImpl (map (\(U.Elt _ v) -> v) mels, vt)
      ksS <- liftEither $ ensureDistinctAsc id ks
            `onFirst` \msg -> TCFailedOnValue sq (fromSing kt) msg instrPos Nothing
      pure $ zip ksS vals

    typecheckContractValue
      :: forall cp tz. (tz ~ 'T.TContract cp)
      => U.Value -> EpAddress -> Sing cp -> TypeCheckInstr (T.Value tz)
    typecheckContractValue cv (EpAddress addr epName) pc = do

      instrPos <- ask
      let ensureTypeMatches :: forall t'. SingI t' => TypeCheckInstr (cp :~: t')
          ensureTypeMatches = liftEither @_ @TypeCheckInstr $
            first (TCFailedOnValue cv (demote @ty) "wrong contract parameter" instrPos . Just) $
              (withSingI pc $ eqType @cp @t')
      let unsupportedType :: T.BadTypeForScope -> TCError
          unsupportedType reason = TCFailedOnValue cv (fromSing pc)
            "Unsupported type in type argument of 'contract' type" instrPos $
              Just $ UnsupportedTypeForScope (fromSing pc) reason
      case addr of
        KeyAddress _ -> do
          Refl <- ensureTypeMatches @'T.TUnit
          pure $ VContract addr T.sepcPrimitive
        ContractAddress ca -> case mOriginatedContracts of
          Nothing -> liftEither . Left $ unsupportedType T.BtHasContract
          Just originatedContracts -> case M.lookup ca originatedContracts of
            Just (SomeParamType (_ :: Sing cp') paramNotes) ->
              case T.mkEntrypointCall epName paramNotes of
                Nothing ->
                  throwError $
                  TCFailedOnValue cv (demote @ty) "unknown entrypoint" instrPos . Just $
                  EntrypointNotFound epName
                Just (T.MkEntrypointCallRes (_ :: Notes t') epc) -> do
                  Refl <- ensureTypeMatches @t'
                  pure $ VContract addr (T.SomeEpc epc)
            Nothing ->
              throwError $ TCFailedOnValue cv (demote @ty) "Contract literal unknown"
                instrPos (Just $ UnknownContract addr)

withComparable
  :: forall a (t :: T.T) ty. Sing a
  -> U.Value
  -> Sing t
  -> (T.Comparable a => TypeCheckInstr ty)
  -> TypeCheckInstr ty
withComparable s uv t act = case T.getComparableProofS s of
  Just Dict -> act
  Nothing -> do
    instrPos <- ask
    liftEither . Left $
      TCFailedOnValue uv (fromSing t) "Require a comparable type here" instrPos Nothing

withBigMapAbsence
  :: forall a (t :: T.T) ty. Sing a
  -> U.Value
  -> Sing t
  -> (T.HasNoBigMap a => TypeCheckInstr ty)
  -> TypeCheckInstr ty
withBigMapAbsence s uv t act = case T.bigMapAbsense s of
  Just Dict -> act
  Nothing -> do
    instrPos <- ask
    liftEither . Left $
      TCFailedOnValue uv (fromSing t) "Require a type which doesn't contain `big_map` here"
        instrPos Nothing