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
type TCEnvs = '[TypeCheckEnv, TypeCheckOptions]
type TypeCheck = MultiReaderT TCEnvs (Except TCError)
type TypeCheckNoExcept = MultiReaderT TCEnvs Identity
type TypeCheckResult = ReaderT TypeCheckOptions (Except TCError)
type TCInstrEnvs = TypeCheckInstrEnv ': TCEnvs
type TypeCheckInstr = MultiReaderT TCInstrEnvs (Except TCError)
type TypeCheckInstrNoExcept = MultiReaderT TCInstrEnvs Identity
data SomeParamType = forall t. (T.ParameterScope t) =>
SomeParamType (T.ParamNotes t)
deriving stock instance Show SomeParamType
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
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
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
data TypeCheckMode
= TypeCheckValue
(U.Value, T.T)
(Maybe BigMapFinder)
| TypeCheckContract SomeParamType
| TypeCheckTest
data TypeCheckEnv = TypeCheckEnv
{ TypeCheckEnv -> TypeCheckMode
tcMode :: ~TypeCheckMode
}
type BigMapFinder = Natural -> Maybe SomeVBigMap
data TypeCheckOptions = TypeCheckOptions
{ TypeCheckOptions -> Bool
tcVerbose :: Bool
, TypeCheckOptions -> Bool
tcStrict :: Bool
}
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
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)
-> (b -> TypeCheckInstrNoExcept a)
-> TypeCheckInstr b
-> TypeCheckInstrNoExcept a
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
preserving
:: TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> ([TypeCheckedOp] -> TypeCheckedInstr)
-> (SomeInstr inp -> TypeCheckInstr (SomeInstr inp'))
-> 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))
preserving'
:: TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> ([TypeCheckedOp] -> TypeCheckedInstr)
-> (SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))
-> 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)
guarding
:: U.ExpandedInstr
-> TypeCheckInstr a
-> (a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> 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)
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)
type TcInstrHandler
= forall inp. (T.SingI inp)
=> U.ExpandedInstr
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)