module Morley.Michelson.TypeCheck.TypeCheck
( TcInstrHandler
, TcOriginatedContracts
, TypeCheckEnv(..)
, TypeCheckOptions(..)
, TypeCheck
, TypeCheckNoExcept
, TypeCheckResult
, runTypeCheck
, TypeCheckInstr
, TypeCheckInstrNoExcept
, runTypeCheckIsolated
, runTypeCheckInstrIsolated
, typeCheckingWith
, liftNoExcept
, liftNoExcept'
, throwingTCError
, throwingTCError'
, preserving
, preserving'
, guarding
, guarding_
, tcEither
, tcExtFramesL
, tcModeL
, TypeCheckMode(..)
, SomeParamType(..)
, mkSomeParamType
, unsafeMkSomeParamType
) where
import Control.Monad.Except (Except, mapExceptT, runExcept, throwError)
import Control.Monad.Reader (mapReaderT)
import Data.Default (Default(..))
import Data.Singletons (Sing)
import Fmt (Buildable, build, pretty)
import qualified Text.Show
import Morley.Michelson.ErrorPos (InstrCallStack)
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 (SingI)
import qualified Morley.Michelson.Typed as T
import qualified Morley.Michelson.Untyped as U
import Morley.Tezos.Address (ContractHash)
import Morley.Util.Lens
type TypeCheck =
(ReaderT TypeCheckOptions
(ExceptT TCError
(State TypeCheckEnv)))
type TypeCheckNoExcept =
(ReaderT TypeCheckOptions
(State TypeCheckEnv))
type TypeCheckResult =
(ReaderT TypeCheckOptions
(Except TCError))
data SomeParamType = forall t. (T.ParameterScope t) =>
SomeParamType (Sing t) (T.ParamNotes t)
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
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 Sing t
s 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 (Sing t -> Notes t -> Ty
forall (t :: T). SingI t => Sing t -> Notes t -> Ty
T.AsUTypeExt Sing t
s Notes t
pnNotes) RootAnn
pnRootAnn
unsafeMkSomeParamType :: HasCallStack => U.ParameterType -> SomeParamType
unsafeMkSomeParamType :: ParameterType -> SomeParamType
unsafeMkSomeParamType ParameterType
p =
case ParameterType -> Either TCError SomeParamType
mkSomeParamType ParameterType
p of
Right SomeParamType
sp -> SomeParamType
sp
Left TCError
err -> Text -> SomeParamType
forall a. HasCallStack => Text -> a
error (Text -> SomeParamType) -> Text -> SomeParamType
forall a b. (a -> b) -> a -> b
$ Text
"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 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 CheckScope (ParameterScope t) =>
Either BadTypeForScope (Dict (ParameterScope t))
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
$ 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 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)
| TypeCheckContract SomeParamType
| TypeCheckTest
| TypeCheckPack
data TypeCheckEnv = TypeCheckEnv
{ TypeCheckEnv -> TcExtFrames
tcExtFrames :: ~TcExtFrames
, TypeCheckEnv -> TypeCheckMode
tcMode :: ~TypeCheckMode
}
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 }
makeLensesWith postfixLFields ''TypeCheckEnv
runTypeCheck :: TypeCheckMode -> TypeCheck a -> TypeCheckResult a
runTypeCheck :: TypeCheckMode -> TypeCheck a -> TypeCheckResult a
runTypeCheck TypeCheckMode
mode =
(ExceptT TCError (StateT TypeCheckEnv Identity) a
-> ExceptT TCError Identity a)
-> TypeCheck a -> TypeCheckResult a
forall (m :: * -> *) a (n :: * -> *) b r.
(m a -> n b) -> ReaderT r m a -> ReaderT r n b
mapReaderT ((ExceptT TCError (StateT TypeCheckEnv Identity) a
-> ExceptT TCError Identity a)
-> TypeCheck a -> TypeCheckResult a)
-> (ExceptT TCError (StateT TypeCheckEnv Identity) a
-> ExceptT TCError Identity a)
-> TypeCheck a
-> TypeCheckResult a
forall a b. (a -> b) -> a -> b
$ (StateT TypeCheckEnv Identity (Either TCError a)
-> Identity (Either TCError a))
-> ExceptT TCError (StateT TypeCheckEnv Identity) a
-> ExceptT TCError Identity a
forall (m :: * -> *) e a (n :: * -> *) e' b.
(m (Either e a) -> n (Either e' b))
-> ExceptT e m a -> ExceptT e' n b
mapExceptT ((StateT TypeCheckEnv Identity (Either TCError a)
-> Identity (Either TCError a))
-> ExceptT TCError (StateT TypeCheckEnv Identity) a
-> ExceptT TCError Identity a)
-> (StateT TypeCheckEnv Identity (Either TCError a)
-> Identity (Either TCError a))
-> ExceptT TCError (StateT TypeCheckEnv Identity) a
-> ExceptT TCError Identity a
forall a b. (a -> b) -> a -> b
$ TypeCheckEnv
-> StateT TypeCheckEnv Identity (Either TCError a)
-> Identity (Either TCError a)
forall (f :: * -> *) s a. Functor f => s -> StateT s f a -> f a
evaluatingStateT (TcExtFrames -> TypeCheckMode -> TypeCheckEnv
TypeCheckEnv [] TypeCheckMode
mode)
runTypeCheckIsolated :: TypeCheck a -> TypeCheckResult a
runTypeCheckIsolated :: TypeCheck a -> TypeCheckResult a
runTypeCheckIsolated = TypeCheckMode -> TypeCheck a -> TypeCheckResult a
forall a. TypeCheckMode -> TypeCheck a -> TypeCheckResult a
runTypeCheck TypeCheckMode
TypeCheckTest
typeCheckingWith :: TypeCheckOptions -> TypeCheckResult a -> Either TCError a
typeCheckingWith :: 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)
-> (TypeCheckResult a -> Except TCError a)
-> TypeCheckResult a
-> Either TCError a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeCheckOptions -> TypeCheckResult a -> Except TCError a
forall r (m :: * -> *) a. r -> ReaderT r m a -> m a
usingReaderT TypeCheckOptions
options
type TypeCheckInstr =
ReaderT InstrCallStack TypeCheck
type TypeCheckInstrNoExcept =
ReaderT InstrCallStack TypeCheckNoExcept
runTypeCheckInstrIsolated :: TypeCheckInstr a -> TypeCheckResult a
runTypeCheckInstrIsolated :: TypeCheckInstr a -> TypeCheckResult a
runTypeCheckInstrIsolated = TypeCheck a -> TypeCheckResult a
forall a. TypeCheck a -> TypeCheckResult a
runTypeCheckIsolated (TypeCheck a -> TypeCheckResult a)
-> (TypeCheckInstr a -> TypeCheck a)
-> TypeCheckInstr a
-> TypeCheckResult 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 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' 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 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' 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)
-> (b -> TypeCheckInstrNoExcept a)
-> TypeCheckInstr b
-> TypeCheckInstrNoExcept a
tcEither :: (TCError -> TypeCheckInstrNoExcept a)
-> (b -> TypeCheckInstrNoExcept a)
-> TypeCheckInstr b
-> TypeCheckInstrNoExcept a
tcEither TCError -> TypeCheckInstrNoExcept a
onErr b -> TypeCheckInstrNoExcept a
onOk 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
preserving
:: TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> ([TypeCheckedOp] -> TypeCheckedInstr)
-> (SomeInstr inp -> TypeCheckInstr (SomeInstr inp'))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
preserving :: 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 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
(\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))
preserving'
:: TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> ([TypeCheckedOp] -> TypeCheckedInstr)
-> (SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
preserving' :: 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 =
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
(\[TypeCheckedOp]
tcOps 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)
guarding
:: U.ExpandedInstr
-> TypeCheckInstr a
-> (a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
guarding :: ExpandedInstr
-> TypeCheckInstr a
-> (a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
guarding ExpandedInstr
instr TypeCheckInstr a
cond 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
(\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)
guarding_
:: U.ExpandedInstr
-> TypeCheckInstr a
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
guarding_ :: 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 (TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall a b. a -> b -> a
const TypeCheckInstrNoExcept (TypeCheckedSeq inp)
action)
type TcInstrHandler
= forall inp. (SingI inp, HasCallStack)
=> U.ExpandedInstr
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)