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

module 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 Michelson.Text
import Michelson.TypeCheck.Error (TCError(..), TCTypeError(..))
import Michelson.TypeCheck.Helpers
import Michelson.TypeCheck.TypeCheck
  (SomeParamType(..), TcInstrHandler, TcOriginatedContracts, TypeCheckInstr, TypeCheckOptions(..),
  throwingTCError)
import Michelson.TypeCheck.Types
import Michelson.Typed
  (EpAddress(..), Notes(..), SingT(..), Value'(..), starNotes)
import qualified Michelson.Typed as T
import qualified Michelson.Untyped as U
import Tezos.Address (Address(..))
import Tezos.Core
import Tezos.Crypto
import qualified Tezos.Crypto.BLS12381 as BLS
import 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 @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 = doTypeCheckVal
  where
    doTypeCheckVal :: forall tz. SingI tz => U.Value -> TypeCheckInstr (T.Value tz)
    doTypeCheckVal uvalue = case (uvalue, sing @tz) 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 $ fromInteger i of
        Just m -> pure $ VMutez m
        Nothing -> tcFailedOnValue v (fromSing t) "" (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 (fromIntegral 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) -> withSingI pc $ typecheckContractValue cv addr pc
      (cv@(U.ValueBytes (T.parseEpAddressRaw . U.unInternalByteString -> Right addr))
        , STContract pc) -> withSingI pc $ typecheckContractValue cv addr pc

      (cv, s@(STTicket vt)) -> withSingI 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 (demote @tz)
            "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 @'T.TAddress addrV
            dat <- doTypeCheckVal datV
            amountValue <- doTypeCheckVal @'T.TNat amV
            case (addrValue, amountValue) of
              (VAddress (EpAddress addr ep), VNat am) -> do
                unless (U.isDefEpName ep) $
                  tcFailedOnValue cv (demote @tz)
                    "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 (demote @tz)
              "ticket type expects a value of type `(pair address <data> nat)`"
              Nothing

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

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

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

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

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

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

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

      (v@U.ValueNil, s@(STBigMap (st1 :: Sing st) (st2 :: Sing 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 :: Sing st) (vt :: Sing vt))) ->
        withSingI kt $ withSingI vt $
        withComparable kt sq s $ withBigMapAbsence vt sq s $ do
          keyOrderedElts <- typeCheckMapVal mels sq kt
          pure $ VBigMap Nothing (M.fromDistinctAscList keyOrderedElts)

      -- `{ {} }` can be typechecked either as `VLam` or `VList`.
      (U.ValueLambda s, (STList l :: Sing st)) -> withSingI l $
        case emptyLambdaAsList s of
          Just xs -> doTypeCheckVal @st xs
          Nothing -> tcFailedOnValue uvalue (demote @st) "" Nothing

      (U.ValueSeq s, ((STLambda (i :: Sing inp) (o :: Sing out))) :: Sing l) ->
        withSingI i $ withSingI o $ case emptyListAsLambda s of
          Just xs -> doTypeCheckVal @l xs
          Nothing -> tcFailedOnValue uvalue (demote @l) "" 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, 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
      :: forall t . (SingI t)
      => [U.Value]
      -> TypeCheckInstr [T.Value t]
    typeCheckValsImpl mvs =
      fmap reverse $ foldM (\res mv -> (: res) <$> doTypeCheckVal @t mv) [] 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
      :: forall kt vt. (SingI vt)
      => [U.Elt U.ExpandedOp]
      -> U.Value
      -> Sing kt
      -> TypeCheckInstr [(T.Value kt, T.Value vt)]
    typeCheckMapVal mels sq kt = withSingI kt $ withComparable kt sq kt $ do
      instrPos <- ask
      ks <- typeCheckValsImpl @kt (map (\(U.Elt k _) -> k) mels)
      vals <- typeCheckValsImpl @vt (map (\(U.Elt _ v) -> v) mels)
      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