Michelson.TypeCheck.Helpers

Documentation

onLeft :: Either a c -> (a -> b) -> Either b c

deriveSpecialVN :: VarAnn -> FieldAnn -> VarAnn -> VarAnn

Function which derives special annotations for CDR / CAR instructions.

deriveSpecialFNs :: FieldAnn -> FieldAnn -> VarAnn -> VarAnn -> (VarAnn, FieldAnn, FieldAnn)

Function which derives special annotations for PAIR instruction.

Namely, it does following transformation: PAIR % % [ p.a int : p.b int : .. ] ~ [ p (pair (int %a) (int %b) : .. ]

All relevant cases (e.g. PAIR %myf % ) are handled as they should be according to spec.

deriveVN :: VarAnn -> VarAnn -> VarAnn

Append suffix to variable annotation (if it's not empty)

deriveNsOr :: Notes (TOr a b) -> VarAnn -> (Notes a, Notes b, VarAnn, VarAnn)

Function which extracts annotations for or type (for left and right parts).

It extracts field/type annotations and also auto-generates variable annotations if variable annotation is not provided as second argument.

deriveNsOption :: Notes (TOption a) -> VarAnn -> (Notes a, VarAnn)

Function which extracts annotations for option t type.

It extracts field/type annotations and also auto-generates variable annotation for Some case if it is not provided as second argument.

convergeHSTEl :: (Sing t, Notes t, VarAnn) -> (Sing t, Notes t, VarAnn) -> Either AnnConvergeError (Sing t, Notes t, VarAnn)

convergeHST :: HST ts -> HST ts -> Either AnnConvergeError (HST ts)

Combine annotations from two given stack types

hstToTs :: HST st -> [T]

Extract singleton for each single type of the given stack.

eqHST :: forall as bs. (Typeable as, Typeable bs) => HST as -> HST bs -> Either TCTypeError (as :~: bs)

Check whether the given stack types are equal.

eqHST1 :: forall t st. (Typeable st, Typeable t, SingI t) => HST st -> Either TCTypeError (st :~: '[t])

Check whether the given stack has size 1 and its only element matches the given type. This function is a specialized version of eqHST.

lengthHST :: HST xs -> Natural

ensureDistinctAsc :: (Ord b, Show a) => (a -> b) -> [a] -> Either Text [a]

Check whether elements go in strictly ascending order and return the original list (to keep only one pass on the original list).

eqType :: forall (a :: T) (b :: T). Each [Typeable, SingI] [a, b] => Either TCTypeError (a :~: b)

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

checkEqT :: forall (a :: T) (b :: T) ts m. (Each [Typeable, SingI] [a, b], Typeable ts, MonadReader InstrCallStack m, MonadError TCError m) => ExpandedInstr -> HST ts -> Text -> m (a :~: b)

checkEqHST :: forall (a :: [T]) (b :: [T]) ts m. (Typeable a, Typeable b, Typeable ts, MonadReader InstrCallStack m, MonadError TCError m) => HST a -> HST b -> ExpandedInstr -> HST ts -> Text -> m (a :~: b)

onTypeCheckInstrAnnErr :: (MonadReader InstrCallStack m, MonadError TCError m, Typeable ts) => ExpandedInstr -> HST ts -> Text -> Either AnnConvergeError a -> m a

onTypeCheckInstrTypeErr :: (MonadReader InstrCallStack m, MonadError TCError m, Typeable ts) => ExpandedInstr -> HST ts -> Text -> Either TypeConvergeError a -> m a

onTypeCheckInstrErr :: (MonadReader InstrCallStack m, MonadError TCError m) => ExpandedInstr -> SomeHST -> Text -> Either TCTypeError a -> m a

typeCheckInstrErr :: (MonadReader InstrCallStack m, MonadError TCError m) => ExpandedInstr -> SomeHST -> Text -> m a

typeCheckImpl :: forall inp. Typeable inp => TcInstrHandler -> [ExpandedOp] -> HST inp -> TypeCheckInstr (SomeInstr inp)

compareTypes :: forall t. (Typeable t, SingI t) => (Sing t, Notes t) -> Type -> Either TCTypeError ()

Check whether typed and untyped types converge

memImpl :: forall (q :: CT) (c :: T) ts inp m. (MonadReader InstrCallStack m, MonadError TCError m, Typeable ts, Typeable (MemOpKey c), SingI (MemOpKey c), MemOp c, inp ~ (Tc q ': (c ': ts))) => ExpandedInstr -> HST inp -> VarAnn -> m (SomeInstr inp)

Generic implementation for MEMeration

getImpl :: forall c getKey rs inp m. (GetOp c, Typeable (GetOpKey c), Typeable (GetOpVal c), SingI (GetOpVal c), SingI (GetOpKey c), inp ~ (getKey ': (c ': rs)), MonadReader InstrCallStack m, MonadError TCError m) => ExpandedInstr -> HST (getKey ': (c ': rs)) -> Sing (GetOpVal c) -> Notes (GetOpVal c) -> VarAnn -> m (SomeInstr inp)

updImpl :: forall c updKey updParams rs inp m. (UpdOp c, Typeable (UpdOpKey c), SingI (UpdOpKey c), Typeable (UpdOpParams c), SingI (UpdOpParams c), inp ~ (updKey ': (updParams ': (c ': rs))), MonadReader InstrCallStack m, MonadError TCError m) => ExpandedInstr -> HST (updKey ': (updParams ': (c ': rs))) -> m (SomeInstr inp)

sliceImpl :: (SliceOp c, Typeable c, inp ~ (Tc CNat ': (Tc CNat ': (c ': rs))), Monad m) => HST inp -> VarAnn -> m (SomeInstr inp)

concatImpl :: (ConcatOp c, Typeable c, inp ~ (c ': (c ': rs)), MonadReader InstrCallStack m, MonadError TCError m) => HST inp -> VarAnn -> m (SomeInstr inp)

concatImpl' :: (ConcatOp c, Typeable c, inp ~ (TList c ': rs), Monad m) => HST inp -> VarAnn -> m (SomeInstr inp)

sizeImpl :: (SizeOp c, inp ~ (c ': rs), Monad m) => HST inp -> VarAnn -> m (SomeInstr inp)

arithImpl :: (Typeable (ArithRes aop n m), SingI (ArithRes aop n m), Typeable (Tc (ArithRes aop n m) ': s), inp ~ (Tc n ': (Tc m ': s)), Monad t) => Instr inp (Tc (ArithRes aop n m) ': s) -> HST inp -> VarAnn -> t (SomeInstr inp)

Helper function to construct instructions for binary arithmetic operations.

addImpl :: forall a b inp rs m. (Typeable rs, Each [Typeable, SingI] [a, b], inp ~ (Tc a ': (Tc b ': rs)), MonadReader InstrCallStack m, MonadError TCError m) => Sing a -> Sing b -> HST inp -> VarAnn -> m (SomeInstr inp)

subImpl :: forall a b inp rs m. (Typeable rs, Each [Typeable, SingI] [a, b], inp ~ (Tc a ': (Tc b ': rs)), MonadReader InstrCallStack m, MonadError TCError m) => Sing a -> Sing b -> HST inp -> VarAnn -> m (SomeInstr inp)

mulImpl :: forall a b inp rs m. (Typeable rs, Each [Typeable, SingI] [a, b], inp ~ (Tc a ': (Tc b ': rs)), MonadReader InstrCallStack m, MonadError TCError m) => Sing a -> Sing b -> HST inp -> VarAnn -> m (SomeInstr inp)

edivImpl :: forall a b inp rs m. (Typeable rs, Each [Typeable, SingI] [a, b], inp ~ (Tc a ': (Tc b ': rs)), MonadReader InstrCallStack m, MonadError TCError m) => Sing a -> Sing b -> HST inp -> VarAnn -> m (SomeInstr inp)

compareImpl :: forall a b inp rs m. (Typeable rs, Each [Typeable, SingI] [a, b], inp ~ (Tc a ': (Tc b ': rs)), MonadReader InstrCallStack m, MonadError TCError m) => Sing a -> Sing b -> HST inp -> VarAnn -> m (SomeInstr inp)

unaryArithImpl :: (Typeable (UnaryArithRes aop n), SingI (UnaryArithRes aop n), Typeable (Tc (UnaryArithRes aop n) ': s), inp ~ (Tc n ': s), Monad t) => Instr inp (Tc (UnaryArithRes aop n) ': s) -> HST inp -> VarAnn -> t (SomeInstr inp)

Helper function to construct instructions for binary arithmetic operations.