Safe Haskell	Safe-Inferred
Language	Haskell2010

Morley.Michelson.TypeCheck.TypeCheck

Synopsis

type TcInstr op instr = forall inp. SingI inp => instr -> HST inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
type TcInstrBase op = TcInstr op op
type TcOriginatedContracts = Map ContractHash SomeParamType
data TypeCheckEnv op = TypeCheckEnv {
- tcMode :: ~(TypeCheckMode op)
}
type BigMapFinder = Natural -> Maybe SomeVBigMap
data TypeCheckOptions = TypeCheckOptions {
- tcVerbose :: Bool
- tcStrict :: Bool
}
type TypeCheck op = MultiReaderT (TCEnvs op) (Except (TcError' op))
type TypeCheckNoExcept op = MultiReaderT (TCEnvs op) Identity
type TypeCheckResult op = ReaderT TypeCheckOptions (Except (TcError' op))
runTypeCheck :: TypeCheckMode op -> TypeCheck op a -> TypeCheckResult op a
type TypeCheckInstr op = MultiReaderT (TCInstrEnvs op) (Except (TcError' op))
type TypeCheckInstrNoExcept op = MultiReaderT (TCInstrEnvs op) Identity
runTypeCheckIsolated :: TypeCheck op (SomeTcInstr t) -> TypeCheckResult op (SomeTcInstr t)
typeCheckingWith :: TypeCheckOptions -> TypeCheckResult op a -> Either (TcError' op) a
liftNoExcept :: forall m e (a :: Type). MonadMultiReaderT m Identity => m a -> ChangeMultiReaderBase m (Except e) a
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)
class Data op => IsInstrOp op where
- liftInstr :: InstrAbstract [] op -> op
- pickErrorSrcPos :: op -> Maybe ErrorSrcPos
- tryOpToVal :: op -> Maybe (Value' [] op)
- tryValToOp :: Value' [] op -> Maybe op
preserving :: 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) -> ([TypeCheckedOp op] -> TypeCheckedInstr op) -> (SomeTcInstr inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')) -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
guarding :: IsInstrOp op => InstrAbstract [] op -> TypeCheckInstr op a -> (a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)) -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
guarding_ :: IsInstrOp op => InstrAbstract [] op -> TypeCheckInstr op a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp) -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
tcEither :: (TcError' op -> TypeCheckInstrNoExcept op a) -> (b -> TypeCheckInstrNoExcept op a) -> TypeCheckInstr op b -> TypeCheckInstrNoExcept op a
ask' :: MultiReader n r m => m r
asks' :: forall m r (a :: Type) n. MultiReader n r m => (r -> a) -> m a
local' :: MultiReader n r m => (r -> r) -> m a -> m a
tcModeL :: forall op op. Iso (TypeCheckEnv op) (TypeCheckEnv op) (TypeCheckMode op) (TypeCheckMode op)
data TypeCheckMode op
- = TypeCheckValue (Value' [] op, T) (Maybe BigMapFinder)
- | TypeCheckContract SomeParamType
- | TypeCheckTest
data SomeParamType = forall t.ParameterScope t => SomeParamType (ParamNotes t)
mkSomeParamType :: ParameterType -> Either TcTypeError SomeParamType
data TypeCheckInstrEnv = TypeCheckInstrEnv {
- _tcieErrorPos :: ErrorSrcPos
- _tcieNotInView :: Maybe (Dict IsNotInView)
}
tcieErrorPos :: Lens' TypeCheckInstrEnv ErrorSrcPos
tcieNotInView :: Lens' TypeCheckInstrEnv (Maybe (Dict IsNotInView))

Documentation

type TcInstr op instr = forall inp. SingI inp => instr -> HST inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp) Source #

Some type checker function.

It accepts untyped instructions to typecheck as instr value, and op type stands for the basic operation type like ExpandedOp.

type TcInstrBase op = TcInstr op op Source #

Type checker function for the operation like ExpandedOp. Function of this type we carry in most of the other functions to let them recurse.

type TcOriginatedContracts = Map ContractHash SomeParamType Source #

data TypeCheckEnv op Source #

The typechecking state

Constructors

TypeCheckEnv
Fields tcMode :: ~(TypeCheckMode op)

type BigMapFinder = Natural -> Maybe SomeVBigMap Source #

data TypeCheckOptions Source #

Constructors

TypeCheckOptions

Fields

tcVerbose :: Bool
Whether to add stack type comments after every instruction a la octez-client.
tcStrict :: Bool
Whether should we behave like in test run or real run (real run is more strict).
octez-client run's behaviour can slightly differ from the behaviour of octez-client originate and octez-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.

Instances

Instances details

Default TypeCheckOptions Source #
Instance details Defined in Morley.Michelson.TypeCheck.TypeCheck Methods def :: TypeCheckOptions #

type TypeCheck op = MultiReaderT (TCEnvs op) (Except (TcError' op)) Source #

A full type-check monad carrying intermediary context (via TypeCheckEnv), general TypeCheckOptions and throwing 'TcError''.

type TypeCheckNoExcept op = MultiReaderT (TCEnvs op) Identity Source #

A non-throwing alternative for TypeCheck. Mainly meant to be used for construction of a partially typed tree (see TypeCheckedSeq).

type TypeCheckResult op = ReaderT TypeCheckOptions (Except (TcError' op)) Source #

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.

runTypeCheck :: TypeCheckMode op -> TypeCheck op a -> TypeCheckResult op a Source #

type TypeCheckInstr op = MultiReaderT (TCInstrEnvs op) (Except (TcError' op)) Source #

Version of TypeCheck additionally carrying instruction-specific TypeCheckInstrEnv

type TypeCheckInstrNoExcept op = MultiReaderT (TCInstrEnvs op) Identity Source #

Version of TypeCheckNoExcept additionally carrying instruction-specific TypeCheckInstrEnv

runTypeCheckIsolated :: TypeCheck op (SomeTcInstr t) -> TypeCheckResult op (SomeTcInstr t) Source #

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

typeCheckingWith :: TypeCheckOptions -> TypeCheckResult op a -> Either (TcError' op) a Source #

liftNoExcept :: forall m e (a :: Type). MonadMultiReaderT m Identity => m a -> ChangeMultiReaderBase m (Except e) a Source #

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) Source #

class Data op => IsInstrOp op where Source #

Operation types that appear in AbstractInstr.

Data superclass constraint is used to search for particular sub-instructions.

Methods

liftInstr :: InstrAbstract [] op -> op Source #

Lift a single instruction to operation.

This is used only in error messages.

pickErrorSrcPos :: op -> Maybe ErrorSrcPos Source #

Get callstack at this instruction, if any given.

This is used only in error messages.

tryOpToVal :: op -> Maybe (Value' [] op) Source #

Do our best to re-interpret an instruction as a value.

For instance, { {}, {} } may turn out to be represented both as nested SeqExs and as nested ValueList & ValueNils. This function, along with tryValToOp, let us convert between these two forms.

TODO [#785]: try to remove these two functions

tryValToOp :: Value' [] op -> Maybe op Source #

Do our best to re-interpret a value as an instruction.

This does the opposite to tryOpToVal.

If a value is already a lambda, this can return Nothing.

Instances

Instances details

IsInstrOp ExpandedOp Source #
Instance details Defined in Morley.Michelson.TypeCheck.TypeCheck Methods liftInstr :: InstrAbstract [] ExpandedOp -> ExpandedOp Source # pickErrorSrcPos :: ExpandedOp -> Maybe ErrorSrcPos Source # tryOpToVal :: ExpandedOp -> Maybe (Value' [] ExpandedOp) Source # tryValToOp :: Value' [] ExpandedOp -> Maybe ExpandedOp Source #

preserving Source #

Arguments

:: TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)	Acquiring computation
-> ([TypeCheckedOp op] -> TypeCheckedInstr op)	The parent instruction constructor
-> (SomeTcInstr inp -> TypeCheckInstr op (SomeTcInstr inp'))	The throwing action
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')

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' Source #

Arguments

:: TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)	Acquiring computation
-> ([TypeCheckedOp op] -> TypeCheckedInstr op)	The parent instruction constructor
-> (SomeTcInstr inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp'))	The action
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')

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.

guarding Source #

Arguments

:: IsInstrOp op
=> InstrAbstract [] op	Untyped instruction
-> TypeCheckInstr op a	Acquiring computation
-> (a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))	Follow-up action
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)

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_ :: IsInstrOp op => InstrAbstract [] op -> TypeCheckInstr op a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp) -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp) Source #

Same as guarding but doesn't pass an acquired result to a follow-up action.

tcEither Source #

Arguments

:: (TcError' op -> TypeCheckInstrNoExcept op a)	Call this if the action throws
-> (b -> TypeCheckInstrNoExcept op a)	Call this if it doesn't
-> TypeCheckInstr op b	The action to perform
-> TypeCheckInstrNoExcept op a	A non-throwing action

ask' :: MultiReader n r m => m r Source #

Unconstrained version of ask. Lifts the appropriate number of times depending on the type r.

asks' :: forall m r (a :: Type) n. MultiReader n r m => (r -> a) -> m a Source #

Unconstrained version of asks. asks' f = fmap f ask'.

local' :: MultiReader n r m => (r -> r) -> m a -> m a Source #

Unconstrained version of local. Maps the appropriate number of times depending on the type r.

tcModeL :: forall op op. Iso (TypeCheckEnv op) (TypeCheckEnv op) (TypeCheckMode op) (TypeCheckMode op) Source #

data TypeCheckMode op Source #

Typechecking mode that tells the type checker whether it is typechecking contract code in actual contract, lambda, or test.

Constructors

TypeCheckValue	We're typechecking a value.
Fields (Value' [] op, 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.

data SomeParamType Source #

Constructors

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

Instances

Instances details

Show SomeParamType Source #	`Show` instance of `SomeParamType`, mainly used in test.
Instance details Defined in Morley.Michelson.TypeCheck.TypeCheck Methods showsPrec :: Int -> SomeParamType -> ShowS # show :: SomeParamType -> String # showList :: [SomeParamType] -> ShowS #
Eq SomeParamType Source #	`Eq` instance of `SomeParamType`, mainly used in test.
Instance details Defined in Morley.Michelson.TypeCheck.TypeCheck Methods (==) :: SomeParamType -> SomeParamType -> Bool # (/=) :: SomeParamType -> SomeParamType -> Bool #
Buildable SomeParamType Source #	`Buildable` instance of `SomeParamType`, mainly used in test.
Instance details Defined in Morley.Michelson.TypeCheck.TypeCheck Methods build :: SomeParamType -> Doc buildList :: [SomeParamType] -> Doc

mkSomeParamType :: ParameterType -> Either TcTypeError SomeParamType Source #

data TypeCheckInstrEnv Source #

Constructors

TypeCheckInstrEnv
Fields _tcieErrorPos :: ErrorSrcPos _tcieNotInView :: Maybe (Dict IsNotInView)

Instances

Instances details

Default TypeCheckInstrEnv Source #
Instance details Defined in Morley.Michelson.TypeCheck.TypeCheck Methods def :: TypeCheckInstrEnv #

tcieErrorPos :: Lens' TypeCheckInstrEnv ErrorSrcPos Source #

tcieNotInView :: Lens' TypeCheckInstrEnv (Maybe (Dict IsNotInView)) Source #