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

  , tcContractParamL
  , tcContractsL
  , tcExtFramesL
  ) where

import Control.Monad.Except (withExceptT)
import Control.Monad.Reader (mapReaderT)
import Data.Default (def)

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

type TypeCheck =
  ExceptT TCError
    (State TypeCheckEnv)

type TcOriginatedContracts = Map ContractHash U.ParameterType

-- | The typechecking state
data TypeCheckEnv = TypeCheckEnv
  { TypeCheckEnv -> TcExtFrames
tcExtFrames       :: ~TcExtFrames
  , TypeCheckEnv -> ParameterType
tcContractParam   :: ~U.ParameterType
  , TypeCheckEnv -> TcOriginatedContracts
tcContracts       :: ~TcOriginatedContracts
  }

makeLensesWith postfixLFields ''TypeCheckEnv

runTypeCheck :: U.ParameterType -> TcOriginatedContracts -> TypeCheck a -> Either TCError a
runTypeCheck :: ParameterType
-> TcOriginatedContracts -> TypeCheck a -> Either TCError a
runTypeCheck param :: ParameterType
param contracts :: TcOriginatedContracts
contracts act :: TypeCheck a
act =
  TypeCheckEnv
-> State TypeCheckEnv (Either TCError a) -> Either TCError a
forall s a. s -> State s a -> a
evaluatingState (TcExtFrames
-> ParameterType -> TcOriginatedContracts -> TypeCheckEnv
TypeCheckEnv [] ParameterType
param TcOriginatedContracts
contracts) (State TypeCheckEnv (Either TCError a) -> Either TCError a)
-> State TypeCheckEnv (Either TCError a) -> Either TCError a
forall a b. (a -> b) -> a -> b
$ TypeCheck a -> State TypeCheckEnv (Either TCError a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT TypeCheck a
act

-- | 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 :: TypeCheck a -> Either TCError a
runTypeCheckIsolated = TypeCheckEnv
-> State TypeCheckEnv (Either TCError a) -> Either TCError a
forall s a. s -> State s a -> a
evaluatingState TypeCheckEnv
initSt (State TypeCheckEnv (Either TCError a) -> Either TCError a)
-> (TypeCheck a -> State TypeCheckEnv (Either TCError a))
-> TypeCheck a
-> Either TCError a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeCheck a -> State TypeCheckEnv (Either TCError a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
  where
  initSt :: TypeCheckEnv
initSt =
    TypeCheckEnv :: TcExtFrames
-> ParameterType -> TcOriginatedContracts -> TypeCheckEnv
TypeCheckEnv
    { tcExtFrames :: TcExtFrames
tcExtFrames = []
    , tcContractParam :: ParameterType
tcContractParam = Text -> ParameterType
forall a. HasCallStack => Text -> a
error "Contract param touched"
    , tcContracts :: TcOriginatedContracts
tcContracts = TcOriginatedContracts
forall a. Monoid a => a
mempty
    }

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 :: TypeCheckInstr a -> Either TCError a
runTypeCheckInstrIsolated =
  TypeCheck a -> Either TCError a
forall a. TypeCheck a -> Either TCError a
runTypeCheckIsolated (TypeCheck a -> Either TCError a)
-> (TypeCheckInstr a -> TypeCheck a)
-> TypeCheckInstr a
-> Either TCError a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeCheckInstr a -> InstrCallStack -> TypeCheck a)
-> InstrCallStack -> TypeCheckInstr a -> TypeCheck a
forall a b c. (a -> b -> c) -> b -> a -> c
flip TypeCheckInstr a -> InstrCallStack -> TypeCheck a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT InstrCallStack
forall a. Default a => a
def

-- | Run 'TypeCheckInstr' and modify thrown errors using given functions.
mapTCError :: (TCError -> TCError) -> TypeCheckInstr a -> TypeCheckInstr a
mapTCError :: (TCError -> TCError) -> TypeCheckInstr a -> TypeCheckInstr a
mapTCError f :: TCError -> TCError
f = (ExceptT TCError (State TypeCheckEnv) a
 -> ExceptT TCError (State TypeCheckEnv) a)
-> TypeCheckInstr a -> TypeCheckInstr a
forall (m :: * -> *) a (n :: * -> *) b r.
(m a -> n b) -> ReaderT r m a -> ReaderT r n b
mapReaderT ((TCError -> TCError)
-> ExceptT TCError (State TypeCheckEnv) a
-> ExceptT TCError (State TypeCheckEnv) a
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TCError -> TCError
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
      => U.ExpandedInstr
      -> HST inp
      -> TypeCheckInstr (SomeInstr inp)