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

module Michelson.TypeCheck.TypeCheck
  ( TcInstrHandler
  , TcOriginatedContracts
  , TcResult
  , TypeCheckEnv(..)
  , TypeCheckOptions(..)
  , TypeCheck
  , TypeCheckNoExcept
  , runTypeCheck
  , TypeCheckInstr
  , TypeCheckInstrNoExcept
  , runTypeCheckIsolated
  , runTypeCheckInstrIsolated
  , liftNoExcept
  , liftNoExcept'
  , throwingTCError
  , throwingTCError'
  , preserving
  , preserving'
  , guarding
  , guarding_
  , tcEither

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


import Control.Monad.Except (throwError)
import Data.Default (Default(..))
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.TypeCheckedSeq
  (IllTypedInstr(..), TypeCheckedInstr, TypeCheckedOp(..), TypeCheckedSeq(..), someInstrToOp,
  tcsEither)
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 =
  (ReaderT TypeCheckOptions
    (ExceptT TCError
      (State TypeCheckEnv)))

-- | A non-throwing alternative for @TypeCheck@. Mainly meant to be used for
-- construction of a partially typed tree (see @TypeCheckedSeq@).
type TypeCheckNoExcept =
  (ReaderT TypeCheckOptions
    (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 :: SomeParamType -> String
show = ParameterType -> String
forall b a. (Show a, IsString b) => a -> b
show (ParameterType -> String)
-> (SomeParamType -> ParameterType) -> SomeParamType -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeParamType -> ParameterType
someParamToParameterType

-- | @Eq@ instance of @SomeParamType@, mainly used in test.
instance Eq SomeParamType where
  s1 :: SomeParamType
s1 == :: SomeParamType -> SomeParamType -> Bool
== s2 :: SomeParamType
s2 = SomeParamType -> ParameterType
someParamToParameterType SomeParamType
s1 ParameterType -> ParameterType -> Bool
forall a. Eq a => a -> a -> Bool
== SomeParamType -> ParameterType
someParamToParameterType SomeParamType
s2

-- | @Buildable@ instance of @SomeParamType@, mainly used in test.
instance Buildable SomeParamType where
  build :: SomeParamType -> Builder
build = ParameterType -> Builder
forall p. Buildable p => p -> Builder
build (ParameterType -> Builder)
-> (SomeParamType -> ParameterType) -> SomeParamType -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeParamType -> ParameterType
someParamToParameterType

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

-- | Construct @SomeParamType@ from @ParameterType@, mainly used in test.
mkSomeParamTypeUnsafe :: HasCallStack => U.ParameterType -> SomeParamType
mkSomeParamTypeUnsafe :: ParameterType -> SomeParamType
mkSomeParamTypeUnsafe p :: ParameterType
p =
  case ParameterType -> Either TCError SomeParamType
mkSomeParamType ParameterType
p of
    Right sp :: SomeParamType
sp ->  SomeParamType
sp
    Left err :: TCError
err -> Text -> SomeParamType
forall a. HasCallStack => Text -> a
error (Text -> SomeParamType) -> Text -> SomeParamType
forall a b. (a -> b) -> a -> b
$ "Illegal type in parameter of env contract: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> TCError -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty TCError
err

mkSomeParamType :: U.ParameterType -> Either TCError SomeParamType
mkSomeParamType :: ParameterType -> Either TCError SomeParamType
mkSomeParamType (U.ParameterType t :: Type
t ann :: RootAnn
ann) =
  Type
-> (forall (t :: T).
    KnownT t =>
    Notes t -> Either TCError SomeParamType)
-> Either TCError SomeParamType
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
T.withUType Type
t ((forall (t :: T).
  KnownT t =>
  Notes t -> Either TCError SomeParamType)
 -> Either TCError SomeParamType)
-> (forall (t :: T).
    KnownT t =>
    Notes t -> Either TCError SomeParamType)
-> Either TCError SomeParamType
forall a b. (a -> b) -> a -> b
$ \(Notes t
notescp :: T.Notes t) -> do
    case CheckScope (ParameterScope t) =>
Either BadTypeForScope (Dict (ParameterScope t))
forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
T.checkScope @(T.ParameterScope t) of
      Right T.Dict ->
        case Notes t -> RootAnn -> Either ParamEpError (ParamNotes t)
forall (t :: T).
Notes t -> RootAnn -> Either ParamEpError (ParamNotes t)
T.mkParamNotes Notes t
notescp RootAnn
ann of
          Right paramNotes :: ParamNotes t
paramNotes -> SomeParamType -> Either TCError SomeParamType
forall a b. b -> Either a b
Right (SomeParamType -> Either TCError SomeParamType)
-> SomeParamType -> Either TCError SomeParamType
forall a b. (a -> b) -> a -> b
$ Sing t -> ParamNotes t -> SomeParamType
forall (t :: T).
ParameterScope t =>
Sing t -> ParamNotes t -> SomeParamType
SomeParamType Sing t
forall k (a :: k). SingI a => Sing a
T.sing ParamNotes t
paramNotes
          Left err :: ParamEpError
err ->
            TCError -> Either TCError SomeParamType
forall a b. a -> Either a b
Left (TCError -> Either TCError SomeParamType)
-> TCError -> Either TCError SomeParamType
forall a b. (a -> b) -> a -> b
$ Text -> Maybe TCTypeError -> TCError
TCContractError "invalid parameter declaration: " (Maybe TCTypeError -> TCError) -> Maybe TCTypeError -> TCError
forall a b. (a -> b) -> a -> b
$ TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ ParamEpError -> TCTypeError
IllegalParamDecl ParamEpError
err
      Left err :: BadTypeForScope
err -> TCError -> Either TCError SomeParamType
forall a b. a -> Either a b
Left (TCError -> Either TCError SomeParamType)
-> TCError -> Either TCError SomeParamType
forall a b. (a -> b) -> a -> b
$ Text -> Maybe TCTypeError -> TCError
TCContractError ("Parameter type is invalid: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> BadTypeForScope -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty BadTypeForScope
err) Maybe TCTypeError
forall a. Maybe a
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
  { TypeCheckEnv -> TcExtFrames
tcExtFrames :: ~TcExtFrames
  , TypeCheckEnv -> TypeCheckMode
tcMode :: ~TypeCheckMode
  }

data TypeCheckOptions = TypeCheckOptions
  { TypeCheckOptions -> Bool
tcVerbose :: Bool -- ^ Whether to add stack type comments after every
                      -- instruction a la tezos-client.
  }

instance Default TypeCheckOptions where
  def :: TypeCheckOptions
def = $WTypeCheckOptions :: Bool -> TypeCheckOptions
TypeCheckOptions{ tcVerbose :: Bool
tcVerbose = Bool
False }

makeLensesWith postfixLFields ''TypeCheckEnv

runTypeCheck :: TypeCheckMode -> TypeCheckOptions -> TypeCheck a -> Either TCError a
runTypeCheck :: TypeCheckMode
-> TypeCheckOptions -> TypeCheck a -> Either TCError a
runTypeCheck mode :: TypeCheckMode
mode options :: TypeCheckOptions
options = TypeCheckEnv
-> State TypeCheckEnv (Either TCError a) -> Either TCError a
forall s a. s -> State s a -> a
evaluatingState (TcExtFrames -> TypeCheckMode -> TypeCheckEnv
TypeCheckEnv [] TypeCheckMode
mode)
                          (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
. ExceptT TCError (StateT TypeCheckEnv Identity) a
-> State TypeCheckEnv (Either TCError a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
                          (ExceptT TCError (StateT TypeCheckEnv Identity) a
 -> State TypeCheckEnv (Either TCError a))
-> (TypeCheck a
    -> ExceptT TCError (StateT TypeCheckEnv Identity) a)
-> TypeCheck a
-> State TypeCheckEnv (Either TCError a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeCheckOptions
-> TypeCheck a -> ExceptT TCError (StateT TypeCheckEnv Identity) a
forall r (m :: * -> *) a. r -> ReaderT r m a -> m a
usingReaderT TypeCheckOptions
options

-- | 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 = TypeCheckMode
-> TypeCheckOptions -> TypeCheck a -> Either TCError a
forall a.
TypeCheckMode
-> TypeCheckOptions -> TypeCheck a -> Either TCError a
runTypeCheck TypeCheckMode
TypeCheckTest TypeCheckOptions
forall a. Default a => a
def

type TcResult inp = Either TCError (SomeInstr inp)

type TypeCheckInstr =
  ReaderT InstrCallStack TypeCheck

type TypeCheckInstrNoExcept =
  ReaderT InstrCallStack TypeCheckNoExcept

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

liftNoExcept :: TypeCheckInstrNoExcept a -> TypeCheckInstr a
liftNoExcept :: TypeCheckInstrNoExcept a -> TypeCheckInstr a
liftNoExcept action :: TypeCheckInstrNoExcept a
action = (TypeCheckInstrNoExcept a
-> ReaderT InstrCallStack TypeCheck (TypeCheckInstrNoExcept a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeCheckInstrNoExcept a
action)
                 ReaderT InstrCallStack TypeCheck (TypeCheckInstrNoExcept a)
-> ReaderT
     InstrCallStack
     TypeCheck
     (TypeCheckInstrNoExcept a -> TypeCheckNoExcept a)
-> ReaderT InstrCallStack TypeCheck (TypeCheckNoExcept a)
forall (f :: * -> *) a b. Applicative f => f a -> f (a -> b) -> f b
<**> (InstrCallStack -> TypeCheckInstrNoExcept a -> TypeCheckNoExcept a
forall r (m :: * -> *) a. r -> ReaderT r m a -> m a
usingReaderT (InstrCallStack -> TypeCheckInstrNoExcept a -> TypeCheckNoExcept a)
-> ReaderT InstrCallStack TypeCheck InstrCallStack
-> ReaderT
     InstrCallStack
     TypeCheck
     (TypeCheckInstrNoExcept a -> TypeCheckNoExcept a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT InstrCallStack TypeCheck InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask)
                 ReaderT InstrCallStack TypeCheck (TypeCheckNoExcept a)
-> ReaderT
     InstrCallStack
     TypeCheck
     (TypeCheckNoExcept a -> State TypeCheckEnv a)
-> ReaderT InstrCallStack TypeCheck (State TypeCheckEnv a)
forall (f :: * -> *) a b. Applicative f => f a -> f (a -> b) -> f b
<**> (TypeCheckOptions -> TypeCheckNoExcept a -> State TypeCheckEnv a
forall r (m :: * -> *) a. r -> ReaderT r m a -> m a
usingReaderT (TypeCheckOptions -> TypeCheckNoExcept a -> State TypeCheckEnv a)
-> ReaderT InstrCallStack TypeCheck TypeCheckOptions
-> ReaderT
     InstrCallStack
     TypeCheck
     (TypeCheckNoExcept a -> State TypeCheckEnv a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeCheck TypeCheckOptions
-> ReaderT InstrCallStack TypeCheck TypeCheckOptions
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TypeCheck TypeCheckOptions
forall r (m :: * -> *). MonadReader r m => m r
ask)
                 ReaderT InstrCallStack TypeCheck (State TypeCheckEnv a)
-> ReaderT InstrCallStack TypeCheck (State TypeCheckEnv a -> a)
-> TypeCheckInstr a
forall (f :: * -> *) a b. Applicative f => f a -> f (a -> b) -> f b
<**> (TypeCheckEnv -> State TypeCheckEnv a -> a
forall s a. s -> State s a -> a
evaluatingState (TypeCheckEnv -> State TypeCheckEnv a -> a)
-> ReaderT InstrCallStack TypeCheck TypeCheckEnv
-> ReaderT InstrCallStack TypeCheck (State TypeCheckEnv a -> a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT InstrCallStack TypeCheck TypeCheckEnv
forall s (m :: * -> *). MonadState s m => m s
get)

liftNoExcept' :: TypeCheckNoExcept a -> TypeCheck a
liftNoExcept' :: TypeCheckNoExcept a -> TypeCheck a
liftNoExcept' action :: TypeCheckNoExcept a
action = (TypeCheckNoExcept a
-> ReaderT
     TypeCheckOptions
     (ExceptT TCError (StateT TypeCheckEnv Identity))
     (TypeCheckNoExcept a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeCheckNoExcept a
action)
                  ReaderT
  TypeCheckOptions
  (ExceptT TCError (StateT TypeCheckEnv Identity))
  (TypeCheckNoExcept a)
-> ReaderT
     TypeCheckOptions
     (ExceptT TCError (StateT TypeCheckEnv Identity))
     (TypeCheckNoExcept a -> State TypeCheckEnv a)
-> ReaderT
     TypeCheckOptions
     (ExceptT TCError (StateT TypeCheckEnv Identity))
     (State TypeCheckEnv a)
forall (f :: * -> *) a b. Applicative f => f a -> f (a -> b) -> f b
<**> (TypeCheckOptions -> TypeCheckNoExcept a -> State TypeCheckEnv a
forall r (m :: * -> *) a. r -> ReaderT r m a -> m a
usingReaderT (TypeCheckOptions -> TypeCheckNoExcept a -> State TypeCheckEnv a)
-> TypeCheck TypeCheckOptions
-> ReaderT
     TypeCheckOptions
     (ExceptT TCError (StateT TypeCheckEnv Identity))
     (TypeCheckNoExcept a -> State TypeCheckEnv a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeCheck TypeCheckOptions
forall r (m :: * -> *). MonadReader r m => m r
ask)
                  ReaderT
  TypeCheckOptions
  (ExceptT TCError (StateT TypeCheckEnv Identity))
  (State TypeCheckEnv a)
-> ReaderT
     TypeCheckOptions
     (ExceptT TCError (StateT TypeCheckEnv Identity))
     (State TypeCheckEnv a -> a)
-> TypeCheck a
forall (f :: * -> *) a b. Applicative f => f a -> f (a -> b) -> f b
<**> (TypeCheckEnv -> State TypeCheckEnv a -> a
forall s a. s -> State s a -> a
evaluatingState (TypeCheckEnv -> State TypeCheckEnv a -> a)
-> ReaderT
     TypeCheckOptions
     (ExceptT TCError (StateT TypeCheckEnv Identity))
     TypeCheckEnv
-> ReaderT
     TypeCheckOptions
     (ExceptT TCError (StateT TypeCheckEnv Identity))
     (State TypeCheckEnv a -> a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT
  TypeCheckOptions
  (ExceptT TCError (StateT TypeCheckEnv Identity))
  TypeCheckEnv
forall s (m :: * -> *). MonadState s m => m s
get)

throwingTCError
  :: TypeCheckInstrNoExcept (TypeCheckedSeq inp) -> TypeCheckInstr (SomeInstr inp)
throwingTCError :: TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> TypeCheckInstr (SomeInstr inp)
throwingTCError action :: TypeCheckInstrNoExcept (TypeCheckedSeq inp)
action = TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> TypeCheckInstr (TypeCheckedSeq inp)
forall a. TypeCheckInstrNoExcept a -> TypeCheckInstr a
liftNoExcept TypeCheckInstrNoExcept (TypeCheckedSeq inp)
action
  TypeCheckInstr (TypeCheckedSeq inp)
-> (TypeCheckedSeq inp -> TypeCheckInstr (SomeInstr inp))
-> TypeCheckInstr (SomeInstr inp)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([TypeCheckedOp] -> TCError -> TypeCheckInstr (SomeInstr inp))
-> (SomeInstr inp -> TypeCheckInstr (SomeInstr inp))
-> TypeCheckedSeq inp
-> TypeCheckInstr (SomeInstr inp)
forall a (inp :: [T]).
([TypeCheckedOp] -> TCError -> a)
-> (SomeInstr inp -> a) -> TypeCheckedSeq inp -> a
tcsEither ((TCError -> TypeCheckInstr (SomeInstr inp))
-> [TypeCheckedOp] -> TCError -> TypeCheckInstr (SomeInstr inp)
forall a b. a -> b -> a
const TCError -> TypeCheckInstr (SomeInstr inp)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError) (SomeInstr inp -> TypeCheckInstr (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure)

throwingTCError'
  :: TypeCheckNoExcept (TypeCheckedSeq inp) -> TypeCheck (SomeInstr inp)
throwingTCError' :: TypeCheckNoExcept (TypeCheckedSeq inp) -> TypeCheck (SomeInstr inp)
throwingTCError' action :: TypeCheckNoExcept (TypeCheckedSeq inp)
action = TypeCheckNoExcept (TypeCheckedSeq inp)
-> TypeCheck (TypeCheckedSeq inp)
forall a. TypeCheckNoExcept a -> TypeCheck a
liftNoExcept' TypeCheckNoExcept (TypeCheckedSeq inp)
action
  TypeCheck (TypeCheckedSeq inp)
-> (TypeCheckedSeq inp -> TypeCheck (SomeInstr inp))
-> TypeCheck (SomeInstr inp)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([TypeCheckedOp] -> TCError -> TypeCheck (SomeInstr inp))
-> (SomeInstr inp -> TypeCheck (SomeInstr inp))
-> TypeCheckedSeq inp
-> TypeCheck (SomeInstr inp)
forall a (inp :: [T]).
([TypeCheckedOp] -> TCError -> a)
-> (SomeInstr inp -> a) -> TypeCheckedSeq inp -> a
tcsEither ((TCError -> TypeCheck (SomeInstr inp))
-> [TypeCheckedOp] -> TCError -> TypeCheck (SomeInstr inp)
forall a b. a -> b -> a
const TCError -> TypeCheck (SomeInstr inp)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError) (SomeInstr inp -> TypeCheck (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure)

tcEither
  :: (TCError -> TypeCheckInstrNoExcept a) -- ^ Call this if the action throws
  -> (b -> TypeCheckInstrNoExcept a) -- ^ Call this if it doesn't
  -> TypeCheckInstr b -- ^ The action to perform
  -> TypeCheckInstrNoExcept a -- ^ A non-throwing action
tcEither :: (TCError -> TypeCheckInstrNoExcept a)
-> (b -> TypeCheckInstrNoExcept a)
-> TypeCheckInstr b
-> TypeCheckInstrNoExcept a
tcEither onErr :: TCError -> TypeCheckInstrNoExcept a
onErr onOk :: b -> TypeCheckInstrNoExcept a
onOk action :: TypeCheckInstr b
action = do
  Either TCError b
res <- (TypeCheckInstr b
-> ReaderT InstrCallStack TypeCheckNoExcept (TypeCheckInstr b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeCheckInstr b
action)
    ReaderT InstrCallStack TypeCheckNoExcept (TypeCheckInstr b)
-> ReaderT
     InstrCallStack TypeCheckNoExcept (TypeCheckInstr b -> TypeCheck b)
-> ReaderT InstrCallStack TypeCheckNoExcept (TypeCheck b)
forall (f :: * -> *) a b. Applicative f => f a -> f (a -> b) -> f b
<**> (InstrCallStack -> TypeCheckInstr b -> TypeCheck b
forall r (m :: * -> *) a. r -> ReaderT r m a -> m a
usingReaderT (InstrCallStack -> TypeCheckInstr b -> TypeCheck b)
-> ReaderT InstrCallStack TypeCheckNoExcept InstrCallStack
-> ReaderT
     InstrCallStack TypeCheckNoExcept (TypeCheckInstr b -> TypeCheck b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT InstrCallStack TypeCheckNoExcept InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask)
    ReaderT InstrCallStack TypeCheckNoExcept (TypeCheck b)
-> ReaderT
     InstrCallStack
     TypeCheckNoExcept
     (TypeCheck b -> ExceptT TCError (StateT TypeCheckEnv Identity) b)
-> ReaderT
     InstrCallStack
     TypeCheckNoExcept
     (ExceptT TCError (StateT TypeCheckEnv Identity) b)
forall (f :: * -> *) a b. Applicative f => f a -> f (a -> b) -> f b
<**> (TypeCheckOptions
-> TypeCheck b -> ExceptT TCError (StateT TypeCheckEnv Identity) b
forall r (m :: * -> *) a. r -> ReaderT r m a -> m a
usingReaderT (TypeCheckOptions
 -> TypeCheck b -> ExceptT TCError (StateT TypeCheckEnv Identity) b)
-> ReaderT InstrCallStack TypeCheckNoExcept TypeCheckOptions
-> ReaderT
     InstrCallStack
     TypeCheckNoExcept
     (TypeCheck b -> ExceptT TCError (StateT TypeCheckEnv Identity) b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeCheckNoExcept TypeCheckOptions
-> ReaderT InstrCallStack TypeCheckNoExcept TypeCheckOptions
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TypeCheckNoExcept TypeCheckOptions
forall r (m :: * -> *). MonadReader r m => m r
ask)
    ReaderT
  InstrCallStack
  TypeCheckNoExcept
  (ExceptT TCError (StateT TypeCheckEnv Identity) b)
-> ReaderT
     InstrCallStack
     TypeCheckNoExcept
     (ExceptT TCError (StateT TypeCheckEnv Identity) b
      -> State TypeCheckEnv (Either TCError b))
-> ReaderT
     InstrCallStack
     TypeCheckNoExcept
     (State TypeCheckEnv (Either TCError b))
forall (f :: * -> *) a b. Applicative f => f a -> f (a -> b) -> f b
<**> ((ExceptT TCError (StateT TypeCheckEnv Identity) b
 -> State TypeCheckEnv (Either TCError b))
-> ReaderT
     InstrCallStack
     TypeCheckNoExcept
     (ExceptT TCError (StateT TypeCheckEnv Identity) b
      -> State TypeCheckEnv (Either TCError b))
forall (f :: * -> *) a. Applicative f => a -> f a
pure ExceptT TCError (StateT TypeCheckEnv Identity) b
-> State TypeCheckEnv (Either TCError b)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT)
    ReaderT
  InstrCallStack
  TypeCheckNoExcept
  (State TypeCheckEnv (Either TCError b))
-> ReaderT
     InstrCallStack
     TypeCheckNoExcept
     (State TypeCheckEnv (Either TCError b) -> Either TCError b)
-> ReaderT InstrCallStack TypeCheckNoExcept (Either TCError b)
forall (f :: * -> *) a b. Applicative f => f a -> f (a -> b) -> f b
<**> (TypeCheckEnv
-> State TypeCheckEnv (Either TCError b) -> Either TCError b
forall s a. s -> State s a -> a
evaluatingState (TypeCheckEnv
 -> State TypeCheckEnv (Either TCError b) -> Either TCError b)
-> ReaderT InstrCallStack TypeCheckNoExcept TypeCheckEnv
-> ReaderT
     InstrCallStack
     TypeCheckNoExcept
     (State TypeCheckEnv (Either TCError b) -> Either TCError b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT InstrCallStack TypeCheckNoExcept TypeCheckEnv
forall s (m :: * -> *). MonadState s m => m s
get)
  (TCError -> TypeCheckInstrNoExcept a)
-> (b -> TypeCheckInstrNoExcept a)
-> Either TCError b
-> TypeCheckInstrNoExcept a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TCError -> TypeCheckInstrNoExcept a
onErr b -> TypeCheckInstrNoExcept a
onOk Either TCError b
res

-- | Perform a throwing action on an acquired instruction. Preserve the acquired
-- result by embedding it into a type checking tree with a specified parent
-- instruction.
preserving
  :: TypeCheckInstrNoExcept (TypeCheckedSeq inp)
  -- ^ Acquiring computation
  -> ([TypeCheckedOp] -> TypeCheckedInstr)
  -- ^ The parent instruction constructor
  -> (SomeInstr inp -> TypeCheckInstr (SomeInstr inp'))
  -- ^ The throwing action
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
preserving :: TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> ([TypeCheckedOp] -> TypeCheckedInstr)
-> (SomeInstr inp -> TypeCheckInstr (SomeInstr inp'))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
preserving acquire :: TypeCheckInstrNoExcept (TypeCheckedSeq inp)
acquire con :: [TypeCheckedOp] -> TypeCheckedInstr
con action :: SomeInstr inp -> TypeCheckInstr (SomeInstr inp')
action = TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> ([TypeCheckedOp] -> TypeCheckedInstr)
-> (SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
forall (inp :: [T]) (inp' :: [T]).
TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> ([TypeCheckedOp] -> TypeCheckedInstr)
-> (SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
preserving' TypeCheckInstrNoExcept (TypeCheckedSeq inp)
acquire [TypeCheckedOp] -> TypeCheckedInstr
con
  (\instr :: SomeInstr inp
instr -> SomeInstr inp -> TypeCheckInstr (SomeInstr inp')
action SomeInstr inp
instr TypeCheckInstr (SomeInstr inp')
-> (TypeCheckInstr (SomeInstr inp')
    -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
forall a b. a -> (a -> b) -> b
& (TCError -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))
-> (SomeInstr inp' -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))
-> TypeCheckInstr (SomeInstr inp')
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
forall a b.
(TCError -> TypeCheckInstrNoExcept a)
-> (b -> TypeCheckInstrNoExcept a)
-> TypeCheckInstr b
-> TypeCheckInstrNoExcept a
tcEither
    (\err :: TCError
err -> TypeCheckedSeq inp' -> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq inp'
 -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))
-> TypeCheckedSeq inp'
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
forall a b. (a -> b) -> a -> b
$ TCError -> [IllTypedInstr] -> TypeCheckedSeq inp'
forall (inp :: [T]).
TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
IllTypedSeq TCError
err [TypeCheckedInstr -> IllTypedInstr
SemiTypedInstr (TypeCheckedInstr -> IllTypedInstr)
-> TypeCheckedInstr -> IllTypedInstr
forall a b. (a -> b) -> a -> b
$ [TypeCheckedOp] -> TypeCheckedInstr
con [SomeInstr inp -> TypeCheckedOp
forall (inp :: [T]). SomeInstr inp -> TypeCheckedOp
someInstrToOp SomeInstr inp
instr]])
    (TypeCheckedSeq inp' -> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq inp'
 -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))
-> (SomeInstr inp' -> TypeCheckedSeq inp')
-> SomeInstr inp'
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeInstr inp' -> TypeCheckedSeq inp'
forall (inp :: [T]). SomeInstr inp -> TypeCheckedSeq inp
WellTypedSeq))

-- | Perform a non-throwing action on an acquired instruction. Preserve the
-- acquired result even if the action does not succeed. Embed the result into a
-- type checking tree with a specified parent instruction.
preserving'
  :: TypeCheckInstrNoExcept (TypeCheckedSeq inp)
  -- ^ Acquiring computation
  -> ([TypeCheckedOp] -> TypeCheckedInstr)
  -- ^ The parent instruction constructor
  -> (SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))
  -- ^ The action
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
preserving' :: TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> ([TypeCheckedOp] -> TypeCheckedInstr)
-> (SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
preserving' acquire :: TypeCheckInstrNoExcept (TypeCheckedSeq inp)
acquire con :: [TypeCheckedOp] -> TypeCheckedInstr
con action :: SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
action =
  TypeCheckInstrNoExcept (TypeCheckedSeq inp)
acquire TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> (TypeCheckedSeq inp
    -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([TypeCheckedOp]
 -> TCError -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))
-> (SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))
-> TypeCheckedSeq inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
forall a (inp :: [T]).
([TypeCheckedOp] -> TCError -> a)
-> (SomeInstr inp -> a) -> TypeCheckedSeq inp -> a
tcsEither
    (\tcOps :: [TypeCheckedOp]
tcOps err :: TCError
err -> TypeCheckedSeq inp' -> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq inp'
 -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))
-> TypeCheckedSeq inp'
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
forall a b. (a -> b) -> a -> b
$ TCError -> [IllTypedInstr] -> TypeCheckedSeq inp'
forall (inp :: [T]).
TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
IllTypedSeq TCError
err [TypeCheckedInstr -> IllTypedInstr
SemiTypedInstr (TypeCheckedInstr -> IllTypedInstr)
-> TypeCheckedInstr -> IllTypedInstr
forall a b. (a -> b) -> a -> b
$ [TypeCheckedOp] -> TypeCheckedInstr
con [TypeCheckedOp]
tcOps])
    (SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
action)

-- | Acquire a resource. If successfully, call a follow-up action on it,
-- otherwise embed the error into a type checking tree along with a specified
-- untyped instruction.
guarding
  :: U.ExpandedInstr -- ^ Untyped instruction
  -> TypeCheckInstr a -- ^ Acquiring computation
  -> (a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)) -- ^ Follow-up action
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
guarding :: ExpandedInstr
-> TypeCheckInstr a
-> (a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
guarding instr :: ExpandedInstr
instr cond :: TypeCheckInstr a
cond action :: a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
action = do
  TypeCheckInstr a
cond TypeCheckInstr a
-> (TypeCheckInstr a
    -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall a b. a -> (a -> b) -> b
& (TCError -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> (a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> TypeCheckInstr a
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall a b.
(TCError -> TypeCheckInstrNoExcept a)
-> (b -> TypeCheckInstrNoExcept a)
-> TypeCheckInstr b
-> TypeCheckInstrNoExcept a
tcEither
    (\err :: TCError
err -> TypeCheckedSeq inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> TypeCheckedSeq inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall a b. (a -> b) -> a -> b
$ TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
forall (inp :: [T]).
TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
IllTypedSeq TCError
err [ExpandedOp -> IllTypedInstr
NonTypedInstr (ExpandedOp -> IllTypedInstr) -> ExpandedOp -> IllTypedInstr
forall a b. (a -> b) -> a -> b
$ ExpandedInstr -> ExpandedOp
U.PrimEx ExpandedInstr
instr])
    (a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
action)

-- | Same as @guarding@ but doesn't pass an acquired result to a follow-up
-- action.
guarding_
  :: U.ExpandedInstr
  -> TypeCheckInstr a
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
guarding_ :: ExpandedInstr
-> TypeCheckInstr a
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
guarding_ instr :: ExpandedInstr
instr cond :: TypeCheckInstr a
cond action :: TypeCheckInstrNoExcept (TypeCheckedSeq inp)
action = ExpandedInstr
-> TypeCheckInstr a
-> (a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall a (inp :: [T]).
ExpandedInstr
-> TypeCheckInstr a
-> (a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
guarding ExpandedInstr
instr TypeCheckInstr a
cond (TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall a b. a -> b -> a
const TypeCheckInstrNoExcept (TypeCheckedSeq inp)
action)

-- 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
      -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)