-- 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.Map as M
import qualified Data.Set as S
import Data.Singletons (Sing, SingI(..), demote)
import Data.Typeable ((:~:)(..))
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, throwingTCError)
import Michelson.TypeCheck.Types
import Michelson.Typed
  (EpAddress(..), KnownT, Notes(..), SingT(..), Value'(..), fromSingT, starNotes)
import qualified Michelson.Typed as T
import qualified Michelson.Untyped as U
import Tezos.Address (Address(..))
import Tezos.Core
import Tezos.Crypto
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 (fromSingT t) "" (Just NegativeNat)
      (v@(U.ValueInt i), t@STMutez) -> case mkMutez $ fromInteger i of
        Just mtz -> pure $ VMutez mtz
        Nothing -> tcFailedOnValue v (fromSingT 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 (fromSingT 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 (fromSingT t) "" (Just $ InvalidAddress err)
      (v@(U.ValueString s), t@STKeyHash) -> case parseKeyHash (unMText s)  of
        Right kHash -> pure $ VKeyHash kHash
        Left err -> tcFailedOnValue v (fromSingT 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 (fromSingT t) "" (Just $ InvalidKeyHash err)
      (v@(U.ValueString s), t@STTimestamp) -> case parseTimestamp $ unMText s of
        Just tstamp -> pure $ VTimestamp tstamp
        Nothing -> tcFailedOnValue v (fromSingT 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

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

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

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

      (U.ValueNil, STSet (s :: Sing st)) -> 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 $ do
        instrPos <- ask

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

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

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

      (v@U.ValueNil, s@(STBigMap (st :: Sing st) _)) ->
        withComparable st v s $ pure $ T.VBigMap M.empty

      (sq@(U.ValueMap (toList -> mels)), s@(STBigMap (kt :: Sing st) _)) -> withComparable kt sq s $ do
        keyOrderedElts <- typeCheckMapVal mels sq kt
        pure $ VBigMap (M.fromDistinctAscList keyOrderedElts)

      (v, STLambda (_ :: Sing it) (_ :: Sing ot)) -> 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 (fromSingT t) "unknown value" Nothing

    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) -> tcFailedOnValue uvalue (fromSingT $ sing @ty)
                  ("Value is not well typed: " <> show t) 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 kt, SingI vt)
      => [U.Elt U.ExpandedOp]
      -> U.Value
      -> Sing kt
      -> TypeCheckInstr [(T.Value kt, T.Value vt)]
    typeCheckMapVal mels sq 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 (fromSingT kt) msg instrPos Nothing
      pure $ zip ksS vals

    typecheckContractValue
      :: forall cp tz. (Typeable cp, SingI cp, 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'. KnownT t' => TypeCheckInstr (cp :~: t')
          ensureTypeMatches = liftEither @_ @TypeCheckInstr $
            first (TCFailedOnValue cv (demote @ty) "wrong contract parameter" instrPos . Just) $
              eqType @cp @t'
      let unsupportedType :: T.BadTypeForScope -> TCError
          unsupportedType reason = TCFailedOnValue cv (fromSingT pc)
            "Unsupported type in type argument of 'contract' type" instrPos $
              Just $ UnsupportedTypeForScope (fromSingT 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 (fromSingT t) "Require a comparable type here" instrPos Nothing