TypeCheck.hs

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
  { tcExtFrames       :: ~TcExtFrames
  , tcContractParam   :: ~U.ParameterType
  , tcContracts       :: ~TcOriginatedContracts
  }

makeLensesWith postfixLFields ''TypeCheckEnv

runTypeCheck :: U.ParameterType -> TcOriginatedContracts -> TypeCheck a -> Either TCError a
runTypeCheck param contracts act =
  evaluatingState (TypeCheckEnv [] param contracts) $ runExceptT 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 = evaluatingState initSt . runExceptT
  where
  initSt =
    TypeCheckEnv
    { tcExtFrames = []
    , tcContractParam = error "Contract param touched"
    , tcContracts = 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 =
  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
      => U.ExpandedInstr
      -> HST inp
      -> TypeCheckInstr (SomeInstr inp)