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

module Michelson.TypeCheck.TypeCheck
  ( TcInstrHandler
  , TcOriginatedContracts
  , TcResult
  , TypeCheckEnv (..)
  , TypeCheck
  , runTypeCheck
  , TypeCheckInstr
  , runTypeCheckIsolated
  , runTypeCheckInstrIsolated
  , mapTCError

  , tcExtFramesL
  , tcModeL
  , TypeCheckMode(..)
  , SomeParamType(..)
  , mkSomeParamType
  , mkSomeParamTypeUnsafe
  ) where

import Control.Monad.Except (withExceptT)
import Control.Monad.Reader (mapReaderT)
import Data.Default (def)
import Data.Singletons (Sing)
import Fmt (Buildable, build, pretty)
import qualified Text.Show

import Michelson.ErrorPos (InstrCallStack)
import Michelson.TypeCheck.Error (TCError(..), TCTypeError(..))
import Michelson.TypeCheck.Types
import qualified Michelson.Typed as T
import qualified Michelson.Untyped as U
import Tezos.Address (ContractHash)
import Util.Lens

type TypeCheck =
  ExceptT TCError
    (State TypeCheckEnv)

data SomeParamType = forall t. (T.ParameterScope t) =>
  SomeParamType (Sing t) (T.ParamNotes t)

-- | @Show@ instance of @SomeParamType@, mainly used in test.
instance Show SomeParamType where
  show = show . someParamToParameterType

-- | @Eq@ instance of @SomeParamType@, mainly used in test.
instance Eq SomeParamType where
  s1 == s2 = someParamToParameterType s1 == someParamToParameterType s2

-- | @Buildable@ instance of @SomeParamType@, mainly used in test.
instance Buildable SomeParamType where
  build = build . someParamToParameterType

-- | Helper function means to provide a quick way for creating instance
-- of @SomeParamType@ needed in test.
someParamToParameterType :: SomeParamType -> U.ParameterType
someParamToParameterType (SomeParamType s T.ParamNotesUnsafe{..}) =
  U.ParameterType (T.AsUTypeExt s pnNotes) pnRootAnn

-- | Construct @SomeParamType@ from @ParameterType@, mainly used in test.
mkSomeParamTypeUnsafe :: HasCallStack => U.ParameterType -> SomeParamType
mkSomeParamTypeUnsafe p =
  case mkSomeParamType p of
    Right sp ->  sp
    Left err -> error $ "Illegal type in parameter of env contract: " <> pretty err

mkSomeParamType :: U.ParameterType -> Either TCError SomeParamType
mkSomeParamType (U.ParameterType t ann) =
  T.withUType t $ \(notescp :: T.Notes t) -> do
    case T.checkScope @(T.ParameterScope t) of
      Right T.Dict ->
        case T.mkParamNotes notescp ann of
          Right paramNotes -> Right $ SomeParamType T.sing paramNotes
          Left err ->
            Left $ TCContractError "invalid parameter declaration: " $ Just $ IllegalParamDecl err
      Left err -> Left $ TCContractError ("Parameter type is invalid: " <> pretty err) Nothing

type TcOriginatedContracts = Map ContractHash SomeParamType

-- | Typechecking mode that tells the type checker whether it is typechecking
-- contract code in actual contract, lambda, or test.
data TypeCheckMode
  = TypeCheckValue (U.Value, T.T)
  | TypeCheckContract SomeParamType
  | TypeCheckTest
  | TypeCheckPack

-- | The typechecking state
data TypeCheckEnv = TypeCheckEnv
  { tcExtFrames :: ~TcExtFrames
  , tcMode :: ~TypeCheckMode
  }

makeLensesWith postfixLFields ''TypeCheckEnv

runTypeCheck :: TypeCheckMode -> TypeCheck a -> Either TCError a
runTypeCheck mode = evaluatingState (TypeCheckEnv [] mode) . runExceptT

-- | Run type checker as if it worked isolated from other world -
-- no access to environment of the current contract is allowed.
--
-- Use this function for test purposes only or for some utilities when
-- environment does not matter. In particular, it is assumed that
-- whatever we typecheck does not depend on the parameter type of the
-- contract which is being typechecked (because there is no contract
-- that we are typechecking).
runTypeCheckIsolated :: TypeCheck a -> Either TCError a
runTypeCheckIsolated = runTypeCheck TypeCheckTest

type TcResult inp = Either TCError (SomeInstr inp)

type TypeCheckInstr =
       ReaderT InstrCallStack TypeCheck

-- | Similar to 'runTypeCheckIsolated', but for 'TypeCheckInstr.'
runTypeCheckInstrIsolated :: TypeCheckInstr a -> Either TCError a
runTypeCheckInstrIsolated =
  runTypeCheckIsolated . flip runReaderT def

-- | Run 'TypeCheckInstr' and modify thrown errors using given functions.
mapTCError :: (TCError -> TCError) -> TypeCheckInstr a -> TypeCheckInstr a
mapTCError f = mapReaderT (withExceptT f)

-- pva701: it's really painful to add arguments to TcInstrHandler
-- due to necessity to refactor @typeCheckInstr@.
-- Also functions which are being called from @typeCheckInstr@ would
-- have to be refactored too.
-- Therefore, I am using ReaderT over TypeCheck.
type TcInstrHandler
   = forall inp. (Typeable inp, HasCallStack)
      => U.ExpandedInstr
      -> HST inp
      -> TypeCheckInstr (SomeInstr inp)