-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

module Morley.Michelson.TypeCheck.TypeCheck
  ( TcInstrHandler
  , TcOriginatedContracts
  , TypeCheckEnv(..)
  , BigMapFinder
  , TypeCheckOptions(..)
  , TypeCheck
  , TypeCheckNoExcept
  , TypeCheckResult
  , runTypeCheck
  , TypeCheckInstr
  , TypeCheckInstrNoExcept
  , runTypeCheckIsolated
  , typeCheckingWith
  , liftNoExcept
  , throwingTCError
  , preserving
  , preserving'
  , guarding
  , guarding_
  , tcEither
  , ask'
  , asks'
  , local'

  , tcModeL
  , TypeCheckMode(..)
  , SomeParamType(..)
  , mkSomeParamType
  , TypeCheckInstrEnv (..)
  , tcieErrorPos
  , tcieNotInView
  ) where

import Control.Lens (makeLenses)
import Control.Monad.Except (Except, MonadError, runExcept, throwError)
import Data.Constraint (Dict)
import Data.Default (Default(..))
import Fmt (Buildable, build, pretty)

import Morley.Michelson.ErrorPos (ErrorSrcPos)
import Morley.Michelson.TypeCheck.Error (TCError(..), TCTypeError(..))
import Morley.Michelson.TypeCheck.TypeCheckedSeq
  (IllTypedInstr(..), TypeCheckedInstr, TypeCheckedOp(..), TypeCheckedSeq(..), someInstrToOp,
  tcsEither)
import Morley.Michelson.TypeCheck.Types
import Morley.Michelson.Typed qualified as T
import Morley.Michelson.Typed.Existential (SomeVBigMap)
import Morley.Michelson.Untyped qualified as U
import Morley.Tezos.Address (ContractHash)
import Morley.Util.Lens
import Morley.Util.MultiReader

-- | Environments avaliable during typecheck.
type TCEnvs = '[TypeCheckEnv, TypeCheckOptions]

-- | A full type-check monad carrying intermediary context (via 'TypeCheckEnv'),
-- general 'TypeCheckOptions' and throwing 'TCError'.
type TypeCheck = MultiReaderT TCEnvs (Except TCError)

-- | A non-throwing alternative for 'TypeCheck'. Mainly meant to be used for
-- construction of a partially typed tree (see 'TypeCheckedSeq').
type TypeCheckNoExcept = MultiReaderT TCEnvs Identity

-- | Monad for performing some typechecking operations with the same options.
--
-- Unlike 'TypeCheck' monad, this does not carry the context of intra-contract
-- or intra-value typechecking.
type TypeCheckResult = ReaderT TypeCheckOptions (Except TCError)

-- | Environments available during instr typecheck
type TCInstrEnvs = TypeCheckInstrEnv ': TCEnvs

-- | Version of 'TypeCheck' additionally carrying instruction-specific
-- 'TypeCheckInstrEnv'
type TypeCheckInstr = MultiReaderT TCInstrEnvs (Except TCError)

-- | Version of 'TypeCheckNoExcept' additionally carrying instruction-specific
-- 'TypeCheckInstrEnv'
type TypeCheckInstrNoExcept = MultiReaderT TCInstrEnvs Identity

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

-- | @Show@ instance of @SomeParamType@, mainly used in test.
deriving stock instance Show SomeParamType

-- | @Eq@ instance of @SomeParamType@, mainly used in test.
instance Eq SomeParamType where
  SomeParamType
s1 == :: SomeParamType -> SomeParamType -> Bool
== 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 T.UnsafeParamNotes{RootAnn
Notes t
pnRootAnn :: forall (t :: T). ParamNotes t -> RootAnn
pnNotes :: forall (t :: T). ParamNotes t -> Notes t
pnRootAnn :: RootAnn
pnNotes :: Notes t
..}) =
  Ty -> RootAnn -> ParameterType
U.ParameterType (Notes t -> Ty
forall (t :: T). SingI t => Notes t -> Ty
T.AsUType Notes t
pnNotes) RootAnn
pnRootAnn

mkSomeParamType :: U.ParameterType -> Either TCError SomeParamType
mkSomeParamType :: ParameterType -> Either TCError SomeParamType
mkSomeParamType (U.ParameterType Ty
t RootAnn
ann) =
  Ty
-> (forall (t :: T).
    SingI t =>
    Notes t -> Either TCError SomeParamType)
-> Either TCError SomeParamType
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
T.withUType Ty
t ((forall (t :: T).
  SingI t =>
  Notes t -> Either TCError SomeParamType)
 -> Either TCError SomeParamType)
-> (forall (t :: T).
    SingI t =>
    Notes t -> Either TCError SomeParamType)
-> Either TCError SomeParamType
forall a b. (a -> b) -> a -> b
$ \(Notes t
notescp :: T.Notes t) -> do
    case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
T.checkScope @(T.ParameterScope t) of
      Right Dict (ParameterScope t)
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 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
$ ParamNotes t -> SomeParamType
forall (t :: T). ParameterScope t => ParamNotes t -> SomeParamType
SomeParamType ParamNotes t
paramNotes
          Left 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 Text
"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 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 (Text
"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
    -- ^ We're typechecking a value.
      (U.Value, T.T)
      (Maybe BigMapFinder)
      -- ^ When this is a `Just`, we simulate the typechecking behavior of the RPC's @/run_code@ endpoint.
      --
      -- If an integer is found where a big_map is expected,
      -- we use 'BigMapFinder' to check if a big_map exists with that ID.
      -- If it does, and if the big_map's value and key have the expected types, we replace the
      -- big_map ID with the corresponding big_map value.
  | TypeCheckContract SomeParamType
    -- ^ We're typechecking a contract.
  | TypeCheckTest
    -- ^ We're typechecking a set of instructions in a "test" environment like a REPL,
    -- where the instruction @SELF@ would not make sense.

-- | The typechecking state
data TypeCheckEnv = TypeCheckEnv
  { TypeCheckEnv -> TypeCheckMode
tcMode :: ~TypeCheckMode
  }

type BigMapFinder = Natural -> Maybe SomeVBigMap

data TypeCheckOptions = TypeCheckOptions
  { TypeCheckOptions -> Bool
tcVerbose :: Bool
    -- ^ Whether to add stack type comments after every
    -- instruction a la tezos-client.
  , TypeCheckOptions -> Bool
tcStrict :: Bool
    -- ^ Whether should we behave like in test run or real run
    -- (real run is more strict).
    --
    -- @tezos-client run@'s behaviour can slightly differ from the behaviour
    -- of @tezos-client originate@ and @tezos-client transfer@. For instance,
    -- some values can be "forged" in test run, but not in a real one,
    -- see: Note [Tickets forging].
    --
    -- Set this to @True@ when need to match the behaviour in the network,
    -- and to @False@ if you prefer providing the user with some convenient
    -- features.
  }

instance Default TypeCheckOptions where
  def :: TypeCheckOptions
def = TypeCheckOptions :: Bool -> Bool -> TypeCheckOptions
TypeCheckOptions{ tcVerbose :: Bool
tcVerbose = Bool
False, tcStrict :: Bool
tcStrict = Bool
True }

data TypeCheckInstrEnv = TypeCheckInstrEnv
  { TypeCheckInstrEnv -> ErrorSrcPos
_tcieErrorPos :: ErrorSrcPos
  , TypeCheckInstrEnv -> Maybe (Dict IsNotInView)
_tcieNotInView :: Maybe (Dict T.IsNotInView)
  }

makeLensesWith postfixLFields ''TypeCheckEnv
makeLenses ''TypeCheckInstrEnv

runTypeCheck :: TypeCheckMode -> TypeCheck a -> TypeCheckResult a
runTypeCheck :: forall a. TypeCheckMode -> TypeCheck a -> TypeCheckResult a
runTypeCheck = TypeCheckEnv
-> ReaderT
     TypeCheckEnv
     (ReaderT TypeCheckOptions (ExceptT TCError Identity))
     a
-> ReaderT TypeCheckOptions (ExceptT TCError Identity) a
forall r (m :: * -> *) a. r -> ReaderT r m a -> m a
usingReaderT (TypeCheckEnv
 -> ReaderT
      TypeCheckEnv
      (ReaderT TypeCheckOptions (ExceptT TCError Identity))
      a
 -> ReaderT TypeCheckOptions (ExceptT TCError Identity) a)
-> (TypeCheckMode -> TypeCheckEnv)
-> TypeCheckMode
-> ReaderT
     TypeCheckEnv
     (ReaderT TypeCheckOptions (ExceptT TCError Identity))
     a
-> ReaderT TypeCheckOptions (ExceptT TCError Identity) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeCheckMode -> TypeCheckEnv
TypeCheckEnv

-- | 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 (SomeInstr t) -> TypeCheckResult (SomeInstr t)
runTypeCheckIsolated :: forall (t :: [T]).
TypeCheck (SomeInstr t) -> TypeCheckResult (SomeInstr t)
runTypeCheckIsolated = TypeCheckMode
-> TypeCheck (SomeInstr t) -> TypeCheckResult (SomeInstr t)
forall a. TypeCheckMode -> TypeCheck a -> TypeCheckResult a
runTypeCheck TypeCheckMode
TypeCheckTest

typeCheckingWith :: TypeCheckOptions -> TypeCheckResult a -> Either TCError a
typeCheckingWith :: forall a. TypeCheckOptions -> TypeCheckResult a -> Either TCError a
typeCheckingWith TypeCheckOptions
options = Except TCError a -> Either TCError a
forall e a. Except e a -> Either e a
runExcept (Except TCError a -> Either TCError a)
-> (ReaderT TypeCheckOptions (ExceptT TCError Identity) a
    -> Except TCError a)
-> ReaderT TypeCheckOptions (ExceptT TCError Identity) a
-> Either TCError a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeCheckOptions
-> ReaderT TypeCheckOptions (ExceptT TCError Identity) a
-> Except TCError a
forall r (m :: * -> *) a. r -> ReaderT r m a -> m a
usingReaderT TypeCheckOptions
options

instance Default TypeCheckInstrEnv where
  def :: TypeCheckInstrEnv
def = ErrorSrcPos -> Maybe (Dict IsNotInView) -> TypeCheckInstrEnv
TypeCheckInstrEnv ErrorSrcPos
forall a. Default a => a
def Maybe (Dict IsNotInView)
forall a. Maybe a
Nothing

liftNoExcept
  :: forall m e (a :: Type). MonadMultiReaderT m Identity
  => m a
  -> ChangeMultiReaderBase m (Except e) a
liftNoExcept :: forall (m :: * -> *) e a.
MonadMultiReaderT m Identity =>
m a -> ChangeMultiReaderBase m (Except e) a
liftNoExcept m a
action = (Identity a -> ExceptT e Identity a)
-> m a -> MultiReaderT (MultiReaderIso m) (Except e) a
forall (xs :: [*]) (m' :: * -> *) (m :: * -> *) (n' :: * -> *)
       (n :: * -> *) a b.
(MonadMultiReaderMap xs, m' ~ MultiReaderT xs m,
 n' ~ MultiReaderT xs n, xs ~ MultiReaderIso m') =>
(m a -> n b) -> m' a -> n' b
mapMultiReaderT (forall (f :: * -> *) a. Applicative f => a -> f a
pure @(Except e) (a -> ExceptT e Identity a)
-> (Identity a -> a) -> Identity a -> ExceptT e Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity a -> a
forall a. Identity a -> a
runIdentity) m a
action

throwingTCError
  :: ( MonadMultiReaderT m Identity
     , m' ~ ChangeMultiReaderBase m (Except TCError)
     , MonadError TCError m'
     )
  => m (TypeCheckedSeq inp) -> m' (SomeInstr inp)
throwingTCError :: forall (m :: * -> *) (m' :: * -> *) (inp :: [T]).
(MonadMultiReaderT m Identity,
 m' ~ ChangeMultiReaderBase m (ExceptT TCError Identity),
 MonadError TCError m') =>
m (TypeCheckedSeq inp) -> m' (SomeInstr inp)
throwingTCError m (TypeCheckedSeq inp)
action = forall (m :: * -> *) e a.
MonadMultiReaderT m Identity =>
m a -> ChangeMultiReaderBase m (Except e) a
liftNoExcept @_ @TCError m (TypeCheckedSeq inp)
action m' (TypeCheckedSeq inp)
-> (TypeCheckedSeq inp -> m' (SomeInstr inp)) -> m' (SomeInstr inp)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([TypeCheckedOp] -> TCError -> m' (SomeInstr inp))
-> (SomeInstr inp -> m' (SomeInstr inp))
-> TypeCheckedSeq inp
-> m' (SomeInstr inp)
forall a (inp :: [T]).
([TypeCheckedOp] -> TCError -> a)
-> (SomeInstr inp -> a) -> TypeCheckedSeq inp -> a
tcsEither ((TCError -> m' (SomeInstr inp))
-> [TypeCheckedOp] -> TCError -> m' (SomeInstr inp)
forall a b. a -> b -> a
const TCError -> m' (SomeInstr inp)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError) (SomeInstr inp -> m' (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 :: forall a b.
(TCError -> TypeCheckInstrNoExcept a)
-> (b -> TypeCheckInstrNoExcept a)
-> TypeCheckInstr b
-> TypeCheckInstrNoExcept a
tcEither TCError -> TypeCheckInstrNoExcept a
onErr b -> TypeCheckInstrNoExcept a
onOk TypeCheckInstr b
action = (TCError
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
      a)
-> (b
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
         a)
-> Either TCError b
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TCError
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     a
TCError -> TypeCheckInstrNoExcept a
onErr b
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     a
b -> TypeCheckInstrNoExcept a
onOk (Either TCError b
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
      a)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (Either TCError b)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (ExceptT TCError Identity b -> Identity (Either TCError b))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     b
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (Either TCError b)
forall (xs :: [*]) (m' :: * -> *) (m :: * -> *) (n' :: * -> *)
       (n :: * -> *) a b.
(MonadMultiReaderMap xs, m' ~ MultiReaderT xs m,
 n' ~ MultiReaderT xs n, xs ~ MultiReaderIso m') =>
(m a -> n b) -> m' a -> n' b
mapMultiReaderT (Either TCError b -> Identity (Either TCError b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either TCError b -> Identity (Either TCError b))
-> (ExceptT TCError Identity b -> Either TCError b)
-> ExceptT TCError Identity b
-> Identity (Either TCError b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT TCError Identity b -> Either TCError b
forall e a. Except e a -> Either e a
runExcept) ReaderT
  TypeCheckInstrEnv
  (ReaderT
     TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
  b
TypeCheckInstr b
action

-- | 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 :: forall (inp :: [T]) (inp' :: [T]).
TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> ([TypeCheckedOp] -> TypeCheckedInstr)
-> (SomeInstr inp -> TypeCheckInstr (SomeInstr inp'))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
preserving TypeCheckInstrNoExcept (TypeCheckedSeq inp)
acquire [TypeCheckedOp] -> TypeCheckedInstr
con 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
  (\SomeInstr inp
instr -> SomeInstr inp -> TypeCheckInstr (SomeInstr inp')
action SomeInstr inp
instr ReaderT
  TypeCheckInstrEnv
  (ReaderT
     TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
  (SomeInstr inp')
-> (ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (SomeInstr inp')
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
         (TypeCheckedSeq inp'))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (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
    (\TCError
err -> TypeCheckedSeq inp'
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp')
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq inp'
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
      (TypeCheckedSeq inp'))
-> TypeCheckedSeq inp'
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (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'
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp')
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq inp'
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
      (TypeCheckedSeq inp'))
-> (SomeInstr inp' -> TypeCheckedSeq inp')
-> SomeInstr inp'
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (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' :: 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 SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
action =
  ReaderT
  TypeCheckInstrEnv
  (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
  (TypeCheckedSeq inp)
TypeCheckInstrNoExcept (TypeCheckedSeq inp)
acquire ReaderT
  TypeCheckInstrEnv
  (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
  (TypeCheckedSeq inp)
-> (TypeCheckedSeq inp
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
         (TypeCheckedSeq inp'))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp')
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([TypeCheckedOp]
 -> TCError
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
      (TypeCheckedSeq inp'))
-> (SomeInstr inp
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
         (TypeCheckedSeq inp'))
-> TypeCheckedSeq inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp')
forall a (inp :: [T]).
([TypeCheckedOp] -> TCError -> a)
-> (SomeInstr inp -> a) -> TypeCheckedSeq inp -> a
tcsEither
    (\[TypeCheckedOp]
tcOps TCError
err -> TypeCheckedSeq inp'
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp')
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq inp'
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
      (TypeCheckedSeq inp'))
-> TypeCheckedSeq inp'
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (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
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp')
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 :: forall a (inp :: [T]).
ExpandedInstr
-> TypeCheckInstr a
-> (a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
guarding ExpandedInstr
instr TypeCheckInstr a
cond a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
action = do
  ReaderT
  TypeCheckInstrEnv
  (ReaderT
     TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
  a
TypeCheckInstr a
cond ReaderT
  TypeCheckInstrEnv
  (ReaderT
     TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
  a
-> (ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      a
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
         (TypeCheckedSeq inp))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (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
    (\TCError
err -> TypeCheckedSeq inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq inp
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
      (TypeCheckedSeq inp))
-> TypeCheckedSeq inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (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_ :: forall a (inp :: [T]).
ExpandedInstr
-> TypeCheckInstr a
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
guarding_ ExpandedInstr
instr TypeCheckInstr a
cond 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 (ReaderT
  TypeCheckInstrEnv
  (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
  (TypeCheckedSeq inp)
-> a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall a b. a -> b -> a
const ReaderT
  TypeCheckInstrEnv
  (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
  (TypeCheckedSeq inp)
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. (T.SingI inp)
      => U.ExpandedInstr
      -> HST inp
      -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)