Michelson.TypeCheck

Documentation

typeCheckContract :: ExtC => TcExtHandler -> UntypedContract -> Either TCError SomeContract

typeCheckVal :: ExtC => UntypedValue -> T -> TypeCheckT SomeVal

Function typeCheckVal converts a single Michelson value given in representation from Michelson.Type module to representation in strictly typed GADT.

As a second argument, typeCheckVal accepts expected type of value.

Type checking algorithm pattern-matches on parse value representation, expected type t and constructs Val t value.

If there was no match on a given pair of value and expected type, that is interpreted as input of wrong type and type check finishes with error.

typeCheckList :: ExtC => [ExpandedOp] -> SomeHST -> TypeCheckT SomeInstr

Function typeCheckList converts list of Michelson instructions given in representation from Michelson.Type module to representation in strictly typed GADT.

Types are checked along the way which is neccessary to construct a strictly typed value.

As a second argument, typeCheckList accepts input stack type representation.

typeCheckCVal :: Value op -> CT -> Maybe SomeValC

data HST (ts :: [T]) where

Data type holding type information for stack (Heterogeneous Stack Type).

This data type is used along with instruction data type Instr to carry information about its input and output stack types.

That is, if there is value instr :: Instr inp out, along with this instr one may carry inpHST :: HST inp and outHST :: HST out which will contain whole information about input and output stack types for instr.

Data type HST is very similar to Data.Vinyl.Rec, but is specialized for a particular purpose. In particular, definition of HST (t1 ': t2 ': ... tn ': '[]) requires constraints (Typeable t1, Typeable t2, ..., Typeable tn) as well as constraints (Typeable '[ t1 ], Typeable '[ t1, t2 ], ...). These applications of Typeable class are required for convenient usage of type encoded by HST ts with some functions from Data.Typeable.

Data type HST (Heterogeneous Stack Type) is a heterogenuous list of triples. First element of triple is a type singleton which is due to main motivation behind HST, namely for it to be used as representation of Instr type data for pattern-matching. Second element of triple is a structure, holding field and type annotations for a given type. Third element of triple is an optional variable annotation for the stack element.

Constructors

SNil :: HST '[]

(::&) :: (Typeable xs, Typeable x, SingI x) => (Sing x, Notes x, VarAnn) -> HST xs -> HST (x ': xs) infixr 7

Instances

Show (HST ts)

Defined in Michelson.TypeCheck.Types

Methods

showsPrec :: Int -> HST ts -> ShowS

show :: HST ts -> String

showList :: [HST ts] -> ShowS

data SomeHST where

No-argument type wrapper for HST data type.

Constructors

SomeHST :: Typeable ts => HST ts -> SomeHST

Instances

Show SomeHST

Defined in Michelson.TypeCheck.Types

Methods

showsPrec :: Int -> SomeHST -> ShowS

show :: SomeHST -> String

showList :: [SomeHST] -> ShowS

data SomeInstr where

Data type holding both instruction and type representations of instruction's input and output.

Intput and output stack types are wrapped inside the type and Typeable constraints are provided to allow convenient unwrapping.

Constructors

(:::) :: (Typeable inp, Typeable out) => Instr inp out -> (HST inp, HST out) -> SomeInstr

SiFail :: SomeInstr

Instances

Show InstrExtT => Show SomeInstr

Defined in Michelson.TypeCheck.Types

Methods

showsPrec :: Int -> SomeInstr -> ShowS

show :: SomeInstr -> String

showList :: [SomeInstr] -> ShowS

data SomeVal where

Data type, holding strictly-typed Michelson value along with its type singleton.

Constructors

(::::) :: (SingI t, Typeable t) => Val Instr t -> (Sing t, Notes t) -> SomeVal

data SomeContract where

Constructors

SomeContract :: (Typeable st, SingI st, SingI cp, Typeable cp) => Contract cp st -> HST (ContractInp cp st) -> HST (ContractOut st) -> SomeContract

Instances

Show InstrExtT => Show SomeContract

Defined in Michelson.TypeCheck.Types

Methods

showsPrec :: Int -> SomeContract -> ShowS

show :: SomeContract -> String

showList :: [SomeContract] -> ShowS

data SomeValC where

Data type, holding strictly-typed Michelson value along with its type singleton.

Constructors

(:--:) :: (SingI t, Typeable t) => CVal t -> Sing t -> SomeValC

data TCError

Type check error

Constructors

TCFailedOnInstr ExpandedInstr SomeHST Text

TCFailedOnValue UntypedValue T Text

TCOtherError Text

Instances

Buildable ExpandedInstr => Show TCError

Defined in Michelson.TypeCheck.Types

Methods

showsPrec :: Int -> TCError -> ShowS

show :: TCError -> String

showList :: [TCError] -> ShowS

Buildable ExpandedInstr => Exception TCError

Defined in Michelson.TypeCheck.Types

Methods

toException :: TCError -> SomeException

fromException :: SomeException -> Maybe TCError

displayException :: TCError -> String

Buildable TCError

Defined in Michelson.TypeCheck.Types

Methods

build :: TCError -> Builder

type ExtC = (Show InstrExtT, Eq ExpandedInstrExtU, Typeable InstrExtT, Buildable ExpandedInstr, ConversibleExt)

Constraints on InstrExtT and untyped Instr which are required for type checking

type TcInstrHandler = ExpandedInstr -> SomeHST -> TypeCheckT SomeInstr

type TcExtHandler = ExpandedInstrExtU -> TcExtFrames -> SomeHST -> TypeCheckT (TcExtFrames, Maybe InstrExtT)

Function for typeChecking a nop and updating state TypeCheckT is used because inside inside of TEST_ASSERT could be PRINTSTACKTYPEetc extended instructions.

type TcExtFrames = [(ExpandedInstrExtU, SomeHST)]

State for type checking nop

type TcResult = Either TCError SomeInstr

data TypeCheckEnv

The typechecking state

Constructors

TypeCheckEnv

Fields

• tcExtHandler :: TcExtHandler
• tcExtFrames :: TcExtFrames
• tcContractParam :: Type

type TypeCheckT a = ExceptT TCError (State TypeCheckEnv) a

runTypeCheckT :: TcExtHandler -> Type -> TypeCheckT a -> Either TCError a

eqT' :: forall a b. (Typeable a, Typeable b) => Either Text (a :~: b)

Function eqT' is a simple wrapper around Data.Typeable.eqT suited for use within Either Text a applicative.