module Morley.Michelson.TypeCheck.TypeCheck
( TcInstr
, TcInstrBase
, TcOriginatedContracts
, TypeCheckEnv(..)
, BigMapFinder
, TypeCheckOptions(..)
, TypeCheck
, TypeCheckNoExcept
, TypeCheckResult
, runTypeCheck
, TypeCheckInstr
, TypeCheckInstrNoExcept
, runTypeCheckIsolated
, typeCheckingWith
, liftNoExcept
, throwingTcError
, IsInstrOp (..)
, 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.Data (Data)
import Data.Default (Default(..))
import Data.Singletons (demote)
import Fmt (Buildable, build)
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 op = '[TypeCheckEnv op, TypeCheckOptions]
type TypeCheck op = MultiReaderT (TCEnvs op) (Except (TcError' op))
type TypeCheckNoExcept op = MultiReaderT (TCEnvs op) Identity
type TypeCheckResult op = ReaderT TypeCheckOptions (Except (TcError' op))
type TCInstrEnvs op = TypeCheckInstrEnv ': TCEnvs op
type TypeCheckInstr op = MultiReaderT (TCInstrEnvs op) (Except (TcError' op))
type TypeCheckInstrNoExcept op = MultiReaderT (TCInstrEnvs op) 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 TcTypeError SomeParamType
mkSomeParamType :: ParameterType -> Either TcTypeError SomeParamType
mkSomeParamType (U.ParameterType (T.AsUType (Notes t
notescp :: T.Notes t)) RootAnn
ann) = do
Dict (ParameterScope t)
T.Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
T.checkScope @(T.ParameterScope t)
Either BadTypeForScope (Dict (ParameterScope t))
-> (Either BadTypeForScope (Dict (ParameterScope t))
-> Either TcTypeError (Dict (ParameterScope t)))
-> Either TcTypeError (Dict (ParameterScope t))
forall a b. a -> (a -> b) -> b
& (BadTypeForScope -> TcTypeError)
-> Either BadTypeForScope (Dict (ParameterScope t))
-> Either TcTypeError (Dict (ParameterScope t))
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (T -> BadTypeForScope -> TcTypeError
UnsupportedTypeForScope (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @t))
ParamNotes t
paramNotes <- Notes t -> RootAnn -> Either ParamEpError (ParamNotes t)
forall (t :: T).
Notes t -> RootAnn -> Either ParamEpError (ParamNotes t)
T.mkParamNotes Notes t
notescp RootAnn
ann
Either ParamEpError (ParamNotes t)
-> (Either ParamEpError (ParamNotes t)
-> Either TcTypeError (ParamNotes t))
-> Either TcTypeError (ParamNotes t)
forall a b. a -> (a -> b) -> b
& (ParamEpError -> TcTypeError)
-> Either ParamEpError (ParamNotes t)
-> Either TcTypeError (ParamNotes t)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ParamEpError -> TcTypeError
IllegalParamDecl
return $ ParamNotes t -> SomeParamType
forall (t :: T). ParameterScope t => ParamNotes t -> SomeParamType
SomeParamType ParamNotes t
paramNotes
type TcOriginatedContracts = Map ContractHash SomeParamType
data TypeCheckMode op
= TypeCheckValue
(U.Value' op, T.T)
(Maybe BigMapFinder)
| TypeCheckContract SomeParamType
| TypeCheckTest
data TypeCheckEnv op = TypeCheckEnv
{ forall op. TypeCheckEnv op -> TypeCheckMode op
tcMode :: ~(TypeCheckMode op)
}
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 op -> TypeCheck op a -> TypeCheckResult op a
runTypeCheck :: forall op a.
TypeCheckMode op -> TypeCheck op a -> TypeCheckResult op a
runTypeCheck = TypeCheckEnv op
-> ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity))
a
-> ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity) a
forall r (m :: * -> *) a. r -> ReaderT r m a -> m a
usingReaderT (TypeCheckEnv op
-> ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity))
a
-> ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity) a)
-> (TypeCheckMode op -> TypeCheckEnv op)
-> TypeCheckMode op
-> ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity))
a
-> ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeCheckMode op -> TypeCheckEnv op
forall op. TypeCheckMode op -> TypeCheckEnv op
TypeCheckEnv
runTypeCheckIsolated :: TypeCheck op (SomeTcInstr t) -> TypeCheckResult op (SomeTcInstr t)
runTypeCheckIsolated :: forall op (t :: [T]).
TypeCheck op (SomeTcInstr t) -> TypeCheckResult op (SomeTcInstr t)
runTypeCheckIsolated = TypeCheckMode op
-> TypeCheck op (SomeTcInstr t)
-> TypeCheckResult op (SomeTcInstr t)
forall op a.
TypeCheckMode op -> TypeCheck op a -> TypeCheckResult op a
runTypeCheck TypeCheckMode op
forall op. TypeCheckMode op
TypeCheckTest
typeCheckingWith :: TypeCheckOptions -> TypeCheckResult op a -> Either (TcError' op) a
typeCheckingWith :: forall op a.
TypeCheckOptions -> TypeCheckResult op a -> Either (TcError' op) a
typeCheckingWith TypeCheckOptions
options = Except (TcError' op) a -> Either (TcError' op) a
forall e a. Except e a -> Either e a
runExcept (Except (TcError' op) a -> Either (TcError' op) a)
-> (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity) a
-> Except (TcError' op) a)
-> ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity) a
-> Either (TcError' op) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeCheckOptions
-> ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity) a
-> Except (TcError' op) 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
:: forall op inp m m'.
( MonadMultiReaderT m Identity
, m' ~ ChangeMultiReaderBase m (Except (TcError' op))
, MonadError (TcError' op) m'
)
=> m (TypeCheckedSeq op inp) -> m' (SomeTcInstr inp)
throwingTcError :: forall op (inp :: [T]) (m :: * -> *) (m' :: * -> *).
(MonadMultiReaderT m Identity,
m' ~ ChangeMultiReaderBase m (Except (TcError' op)),
MonadError (TcError' op) m') =>
m (TypeCheckedSeq op inp) -> m' (SomeTcInstr inp)
throwingTcError m (TypeCheckedSeq op inp)
action = forall (m :: * -> *) e a.
MonadMultiReaderT m Identity =>
m a -> ChangeMultiReaderBase m (Except e) a
liftNoExcept @_ @(TcError' op) m (TypeCheckedSeq op inp)
action m' (TypeCheckedSeq op inp)
-> (TypeCheckedSeq op inp -> m' (SomeTcInstr inp))
-> m' (SomeTcInstr inp)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([TypeCheckedOp op] -> TcError' op -> m' (SomeTcInstr inp))
-> (SomeTcInstr inp -> m' (SomeTcInstr inp))
-> TypeCheckedSeq op inp
-> m' (SomeTcInstr inp)
forall op a (inp :: [T]).
([TypeCheckedOp op] -> TcError' op -> a)
-> (SomeTcInstr inp -> a) -> TypeCheckedSeq op inp -> a
tcsEither ((TcError' op -> m' (SomeTcInstr inp))
-> [TypeCheckedOp op] -> TcError' op -> m' (SomeTcInstr inp)
forall a b. a -> b -> a
const TcError' op -> m' (SomeTcInstr inp)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError) (SomeTcInstr inp -> m' (SomeTcInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure)
tcEither
:: (TcError' op -> TypeCheckInstrNoExcept op a)
-> (b -> TypeCheckInstrNoExcept op a)
-> TypeCheckInstr op b
-> TypeCheckInstrNoExcept op a
tcEither :: forall op a b.
(TcError' op -> TypeCheckInstrNoExcept op a)
-> (b -> TypeCheckInstrNoExcept op a)
-> TypeCheckInstr op b
-> TypeCheckInstrNoExcept op a
tcEither TcError' op -> TypeCheckInstrNoExcept op a
onErr b -> TypeCheckInstrNoExcept op a
onOk TypeCheckInstr op b
action = (TcError' op
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
a)
-> (b
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
a)
-> Either (TcError' op) b
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TcError' op
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
a
TcError' op -> TypeCheckInstrNoExcept op a
onErr b
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
a
b -> TypeCheckInstrNoExcept op a
onOk (Either (TcError' op) b
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
a)
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(Either (TcError' op) b)
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (ExceptT (TcError' op) Identity b
-> Identity (Either (TcError' op) b))
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
b
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(Either (TcError' op) 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' op) b -> Identity (Either (TcError' op) b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (TcError' op) b -> Identity (Either (TcError' op) b))
-> (ExceptT (TcError' op) Identity b -> Either (TcError' op) b)
-> ExceptT (TcError' op) Identity b
-> Identity (Either (TcError' op) b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT (TcError' op) Identity b -> Either (TcError' op) b
forall e a. Except e a -> Either e a
runExcept) ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
b
TypeCheckInstr op b
action
class Data op => IsInstrOp op where
liftInstr :: U.InstrAbstract op -> op
pickErrorSrcPos :: op -> Maybe ErrorSrcPos
tryOpToVal :: op -> Maybe (U.Value' op)
tryValToOp :: U.Value' op -> Maybe op
instance IsInstrOp U.ExpandedOp where
liftInstr :: InstrAbstract ExpandedOp -> ExpandedOp
liftInstr = InstrAbstract ExpandedOp -> ExpandedOp
U.PrimEx
pickErrorSrcPos :: ExpandedOp -> Maybe ErrorSrcPos
pickErrorSrcPos = \case
U.WithSrcEx ErrorSrcPos
cs ExpandedOp
_ -> ErrorSrcPos -> Maybe ErrorSrcPos
forall a. a -> Maybe a
Just ErrorSrcPos
cs
ExpandedOp
_ -> Maybe ErrorSrcPos
forall a. Maybe a
Nothing
tryOpToVal :: ExpandedOp -> Maybe (Value' ExpandedOp)
tryOpToVal = \case
U.SeqEx [] -> Value' ExpandedOp -> Maybe (Value' ExpandedOp)
forall a. a -> Maybe a
Just Value' ExpandedOp
forall op. Value' op
U.ValueNil
U.SeqEx [ExpandedOp]
xs -> (NonEmpty $ Value' ExpandedOp) -> Value' ExpandedOp
forall op. (NonEmpty $ Value' op) -> Value' op
U.ValueSeq ((NonEmpty $ Value' ExpandedOp) -> Value' ExpandedOp)
-> ([Value' ExpandedOp] -> NonEmpty $ Value' ExpandedOp)
-> [Value' ExpandedOp]
-> Value' ExpandedOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Value' ExpandedOp] -> NonEmpty $ Value' ExpandedOp
forall l. (FromList l, FromListC l) => [ListElement l] -> l
fromList ([Value' ExpandedOp] -> Value' ExpandedOp)
-> Maybe [Value' ExpandedOp] -> Maybe (Value' ExpandedOp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ExpandedOp -> Maybe (Value' ExpandedOp))
-> [ExpandedOp] -> Maybe [Value' ExpandedOp]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ExpandedOp -> Maybe (Value' ExpandedOp)
forall op. IsInstrOp op => op -> Maybe (Value' op)
tryOpToVal [ExpandedOp]
xs
U.PrimEx {} -> Maybe (Value' ExpandedOp)
forall a. Maybe a
Nothing
U.WithSrcEx ErrorSrcPos
_ ExpandedOp
i -> ExpandedOp -> Maybe (Value' ExpandedOp)
forall op. IsInstrOp op => op -> Maybe (Value' op)
tryOpToVal ExpandedOp
i
tryValToOp :: Value' ExpandedOp -> Maybe ExpandedOp
tryValToOp = \case
Value' ExpandedOp
U.ValueNil -> ExpandedOp -> Maybe ExpandedOp
forall a. a -> Maybe a
Just (ExpandedOp -> Maybe ExpandedOp) -> ExpandedOp -> Maybe ExpandedOp
forall a b. (a -> b) -> a -> b
$ [ExpandedOp] -> ExpandedOp
U.SeqEx []
U.ValueSeq NonEmpty $ Value' ExpandedOp
xs -> [ExpandedOp] -> ExpandedOp
U.SeqEx ([ExpandedOp] -> ExpandedOp)
-> (NonEmpty ExpandedOp -> [ExpandedOp])
-> NonEmpty ExpandedOp
-> ExpandedOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty ExpandedOp -> [ExpandedOp]
forall t. Container t => t -> [Element t]
toList (NonEmpty ExpandedOp -> ExpandedOp)
-> Maybe (NonEmpty ExpandedOp) -> Maybe ExpandedOp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value' ExpandedOp -> Maybe ExpandedOp)
-> (NonEmpty $ Value' ExpandedOp) -> Maybe (NonEmpty ExpandedOp)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Value' ExpandedOp -> Maybe ExpandedOp
forall op. IsInstrOp op => Value' op -> Maybe op
tryValToOp NonEmpty $ Value' ExpandedOp
xs
Value' ExpandedOp
_ -> Maybe ExpandedOp
forall a. Maybe a
Nothing
preserving
:: TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
-> ([TypeCheckedOp op] -> TypeCheckedInstr op)
-> (SomeTcInstr inp -> TypeCheckInstr op (SomeTcInstr inp'))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
preserving :: forall op (inp :: [T]) (inp' :: [T]).
TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
-> ([TypeCheckedOp op] -> TypeCheckedInstr op)
-> (SomeTcInstr inp -> TypeCheckInstr op (SomeTcInstr inp'))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
preserving TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
acquire [TypeCheckedOp op] -> TypeCheckedInstr op
con SomeTcInstr inp -> TypeCheckInstr op (SomeTcInstr inp')
action = TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
-> ([TypeCheckedOp op] -> TypeCheckedInstr op)
-> (SomeTcInstr inp
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp'))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
forall op (inp :: [T]) (inp' :: [T]).
TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
-> ([TypeCheckedOp op] -> TypeCheckedInstr op)
-> (SomeTcInstr inp
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp'))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
preserving' TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
acquire [TypeCheckedOp op] -> TypeCheckedInstr op
con
(\SomeTcInstr inp
instr -> SomeTcInstr inp -> TypeCheckInstr op (SomeTcInstr inp')
action SomeTcInstr inp
instr ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(SomeTcInstr inp')
-> (ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(SomeTcInstr inp')
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp'))
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp')
forall a b. a -> (a -> b) -> b
& (TcError' op -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp'))
-> (SomeTcInstr inp'
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp'))
-> TypeCheckInstr op (SomeTcInstr inp')
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
forall op a b.
(TcError' op -> TypeCheckInstrNoExcept op a)
-> (b -> TypeCheckInstrNoExcept op a)
-> TypeCheckInstr op b
-> TypeCheckInstrNoExcept op a
tcEither
(\TcError' op
err -> TypeCheckedSeq op inp'
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp')
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq op inp'
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp'))
-> TypeCheckedSeq op inp'
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp')
forall a b. (a -> b) -> a -> b
$ TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp'
forall op (inp :: [T]).
TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
IllTypedSeq TcError' op
err [TypeCheckedInstr op -> IllTypedInstr op
forall op. TypeCheckedInstr op -> IllTypedInstr op
SemiTypedInstr (TypeCheckedInstr op -> IllTypedInstr op)
-> TypeCheckedInstr op -> IllTypedInstr op
forall a b. (a -> b) -> a -> b
$ [TypeCheckedOp op] -> TypeCheckedInstr op
con [SomeTcInstr inp -> TypeCheckedOp op
forall (inp :: [T]) op. SomeTcInstr inp -> TypeCheckedOp op
someInstrToOp SomeTcInstr inp
instr]])
(TypeCheckedSeq op inp'
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp')
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq op inp'
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp'))
-> (SomeTcInstr inp' -> TypeCheckedSeq op inp')
-> SomeTcInstr inp'
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeTcInstr inp' -> TypeCheckedSeq op inp'
forall op (inp :: [T]). SomeTcInstr inp -> TypeCheckedSeq op inp
WellTypedSeq))
preserving'
:: TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
-> ([TypeCheckedOp op] -> TypeCheckedInstr op)
-> (SomeTcInstr inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp'))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
preserving' :: forall op (inp :: [T]) (inp' :: [T]).
TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
-> ([TypeCheckedOp op] -> TypeCheckedInstr op)
-> (SomeTcInstr inp
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp'))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
preserving' TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
acquire [TypeCheckedOp op] -> TypeCheckedInstr op
con SomeTcInstr inp
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
action =
ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
acquire ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
-> (TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp'))
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp')
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([TypeCheckedOp op]
-> TcError' op
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp'))
-> (SomeTcInstr inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp'))
-> TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp')
forall op a (inp :: [T]).
([TypeCheckedOp op] -> TcError' op -> a)
-> (SomeTcInstr inp -> a) -> TypeCheckedSeq op inp -> a
tcsEither
(\[TypeCheckedOp op]
tcOps TcError' op
err -> TypeCheckedSeq op inp'
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp')
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq op inp'
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp'))
-> TypeCheckedSeq op inp'
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp')
forall a b. (a -> b) -> a -> b
$ TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp'
forall op (inp :: [T]).
TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
IllTypedSeq TcError' op
err [TypeCheckedInstr op -> IllTypedInstr op
forall op. TypeCheckedInstr op -> IllTypedInstr op
SemiTypedInstr (TypeCheckedInstr op -> IllTypedInstr op)
-> TypeCheckedInstr op -> IllTypedInstr op
forall a b. (a -> b) -> a -> b
$ [TypeCheckedOp op] -> TypeCheckedInstr op
con [TypeCheckedOp op]
tcOps])
(SomeTcInstr inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp')
SomeTcInstr inp
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
action)
guarding
:: IsInstrOp op
=> U.InstrAbstract op
-> TypeCheckInstr op a
-> (a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
guarding :: forall op a (inp :: [T]).
IsInstrOp op =>
InstrAbstract op
-> TypeCheckInstr op a
-> (a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
guarding InstrAbstract op
instr TypeCheckInstr op a
cond a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
action = do
ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
a
TypeCheckInstr op a
cond ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
a
-> (ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
a
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp))
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall a b. a -> (a -> b) -> b
& (TcError' op -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> (a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> TypeCheckInstr op a
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
forall op a b.
(TcError' op -> TypeCheckInstrNoExcept op a)
-> (b -> TypeCheckInstrNoExcept op a)
-> TypeCheckInstr op b
-> TypeCheckInstrNoExcept op a
tcEither
(\TcError' op
err -> TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp))
-> TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall a b. (a -> b) -> a -> b
$ TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
forall op (inp :: [T]).
TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
IllTypedSeq TcError' op
err [op -> IllTypedInstr op
forall op. op -> IllTypedInstr op
NonTypedInstr (op -> IllTypedInstr op) -> op -> IllTypedInstr op
forall a b. (a -> b) -> a -> b
$ InstrAbstract op -> op
forall op. IsInstrOp op => InstrAbstract op -> op
liftInstr InstrAbstract op
instr])
(a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
action)
guarding_
:: IsInstrOp op
=> U.InstrAbstract op
-> TypeCheckInstr op a
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
guarding_ :: forall op a (inp :: [T]).
IsInstrOp op =>
InstrAbstract op
-> TypeCheckInstr op a
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
guarding_ InstrAbstract op
instr TypeCheckInstr op a
cond TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
action = InstrAbstract op
-> TypeCheckInstr op a
-> (a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
forall op a (inp :: [T]).
IsInstrOp op =>
InstrAbstract op
-> TypeCheckInstr op a
-> (a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
guarding InstrAbstract op
instr TypeCheckInstr op a
cond (ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
-> a
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall a b. a -> b -> a
const ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
action)
type TcInstr op instr
= forall inp. (T.SingI inp)
=> instr
-> HST inp
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
type TcInstrBase op = TcInstr op op