Morley.Michelson.TypeCheck.TypeCheck

Documentation

type TcInstrHandler = forall inp. SingI inp => ExpandedInstr -> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)

type TcOriginatedContracts = Map ContractHash SomeParamType

data TypeCheckEnv

The typechecking state

Constructors

TypeCheckEnv

Fields

• tcMode :: ~TypeCheckMode

type BigMapFinder = Natural -> Maybe SomeVBigMap

data TypeCheckOptions

Constructors

TypeCheckOptions

Fields

• tcVerbose :: Bool

  Whether to add stack type comments after every instruction a la tezos-client.

• tcStrict :: Bool

  Whether should we behave like in test run or real run (real run is more strict).

  tezos-client run's behaviour can slightly differ from the behaviour of tezos-client originate and tezos-client transfer. For instance, some values can be "forged" in test run, but not in a real one, see: Note [Tickets forging].

  Set this to True when need to match the behaviour in the network, and to False if you prefer providing the user with some convenient features.

Instances

Default TypeCheckOptions

Defined in Morley.Michelson.TypeCheck.TypeCheck

Methods

def :: TypeCheckOptions

type TypeCheck = MultiReaderT TCEnvs (Except TCError)

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

type TypeCheckNoExcept = MultiReaderT TCEnvs Identity

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

type TypeCheckResult = ReaderT TypeCheckOptions (Except TCError)

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 -> TypeCheck a -> TypeCheckResult a

type TypeCheckInstr = MultiReaderT TCInstrEnvs (Except TCError)

Version of TypeCheck additionally carrying instruction-specific TypeCheckInstrEnv

type TypeCheckInstrNoExcept = MultiReaderT TCInstrEnvs Identity

Version of TypeCheckNoExcept additionally carrying instruction-specific TypeCheckInstrEnv

runTypeCheckIsolated :: TypeCheck (SomeInstr t) -> TypeCheckResult (SomeInstr t)

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 a -> Either TCError a

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

throwingTCError :: (MonadMultiReaderT m Identity, m' ~ ChangeMultiReaderBase m (Except TCError), MonadError TCError m') => m (TypeCheckedSeq inp) -> m' (SomeInstr inp)

preserving

Arguments

:: TypeCheckInstrNoExcept (TypeCheckedSeq inp)

Acquiring computation

-> ([TypeCheckedOp] -> TypeCheckedInstr)

The parent instruction constructor

-> (SomeInstr inp -> TypeCheckInstr (SomeInstr inp'))

The throwing action

-> TypeCheckInstrNoExcept (TypeCheckedSeq 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'

Arguments

:: TypeCheckInstrNoExcept (TypeCheckedSeq inp)

Acquiring computation

-> ([TypeCheckedOp] -> TypeCheckedInstr)

The parent instruction constructor

-> (SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))

The action

-> TypeCheckInstrNoExcept (TypeCheckedSeq 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

Arguments

:: ExpandedInstr

Untyped instruction

-> TypeCheckInstr a

Acquiring computation

-> (a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))

Follow-up action

-> TypeCheckInstrNoExcept (TypeCheckedSeq 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_ :: ExpandedInstr -> TypeCheckInstr a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)

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

tcEither

Arguments

:: (TCError -> TypeCheckInstrNoExcept a)

Call this if the action throws

-> (b -> TypeCheckInstrNoExcept a)

Call this if it doesn't

-> TypeCheckInstr b

The action to perform

-> TypeCheckInstrNoExcept a

A non-throwing action

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

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

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

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

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

tcModeL :: Iso' TypeCheckEnv TypeCheckMode

data TypeCheckMode

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, 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

Constructors

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

Instances

Show SomeParamType

Show instance of SomeParamType, mainly used in test.

Defined in Morley.Michelson.TypeCheck.TypeCheck

Methods

showsPrec :: Int -> SomeParamType -> ShowS

show :: SomeParamType -> String

showList :: [SomeParamType] -> ShowS

Buildable SomeParamType

Buildable instance of SomeParamType, mainly used in test.

Defined in Morley.Michelson.TypeCheck.TypeCheck

Methods

build :: SomeParamType -> Builder

Eq SomeParamType

Eq instance of SomeParamType, mainly used in test.

Defined in Morley.Michelson.TypeCheck.TypeCheck

Methods

(==) :: SomeParamType -> SomeParamType -> Bool

(/=) :: SomeParamType -> SomeParamType -> Bool

mkSomeParamType :: ParameterType -> Either TCError SomeParamType

data TypeCheckInstrEnv

Constructors

TypeCheckInstrEnv

Fields

• _tcieErrorPos :: ErrorSrcPos
• _tcieNotInView :: Maybe (Dict IsNotInView)

Instances

Default TypeCheckInstrEnv

Defined in Morley.Michelson.TypeCheck.TypeCheck

Methods

def :: TypeCheckInstrEnv

tcieErrorPos :: Lens' TypeCheckInstrEnv ErrorSrcPos

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