Morley.Michelson.TypeCheck.Helpers

Documentation

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

Function which derives special annotations for CDR / CAR instructions.

deriveSpecialFNs :: FieldAnn -> FieldAnn -> VarAnn -> 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 :: (Notes t, Dict (WellTyped t), VarAnn) -> (Notes t, Dict (WellTyped t), VarAnn) -> Either AnnConvergeError (Notes t, Dict (WellTyped 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. (SingI as, SingI bs) => HST as -> HST bs -> Either TCTypeError (as :~: bs)

Check whether the given stack types are equal.

eqHST1 :: forall t st. (SingI st, WellTyped 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.

matchHST1 :: forall t st. (SingI st, WellTyped t) => HST st -> Notes t -> Either TCTypeError (st :~: '[t], HST st)

Version of eqHST1 that also checks whether annotations converge like matchTypes.

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

handleError :: MonadError e m => (e -> m a) -> m a -> m a

Flipped version of catchError.

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

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

onTypeCheckInstrAnnErr :: (MonadReader InstrCallStack m, MonadError TCError m, SingI ts) => ExpandedInstr -> HST ts -> Maybe TypeContext -> Either AnnConvergeError a -> m a

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

onScopeCheckInstrErr :: forall (t :: T) m a. (MonadReader InstrCallStack m, MonadError TCError m, SingI t) => ExpandedInstr -> SomeHST -> Maybe TypeContext -> Either BadTypeForScope a -> m a

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

typeCheckInstrErr' :: (MonadReader InstrCallStack m, MonadError TCError m) => ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a

typeCheckImpl :: forall inp. SingI inp => TcInstrHandler -> [ExpandedOp] -> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)

typeCheckImplStripped :: forall inp. SingI inp => TcInstrHandler -> [ExpandedOp] -> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)

Like typeCheckImpl but without the first and the last stack type comments. Useful to reduce duplication of stack type comments.

matchTypes :: forall t1 t2. Each '[SingI] [t1, t2] => Notes t1 -> Notes t2 -> Either TCTypeError (t1 :~: t2, Notes t1)

Check whether given types are structurally equal and annotations converge.

memImpl :: forall c memKey rs inp m. (MemOp c, SingI (MemOpKey c), inp ~ (memKey ': (c ': rs)), SingI rs, MonadReader InstrCallStack m, MonadError TCError m) => Notes (MemOpKey c) -> HST inp -> VarAnn -> m (SomeInstr inp)

Generic implementation for MEMeration

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

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

getUpdImpl :: forall c updKey updParams rs inp m. (UpdOp c, GetOp c, SingI (UpdOpKey c), SingI (GetOpVal c), inp ~ (updKey ': (updParams ': (c ': rs))), SingI rs, GetOpKey c ~ UpdOpKey c, UpdOpParams c ~ 'TOption (GetOpVal c), MonadReader InstrCallStack m, MonadError TCError m) => Notes (UpdOpKey c) -> HST inp -> Notes (UpdOpParams c) -> VarAnn -> m (SomeInstr inp)

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

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

concatImpl' :: (ConcatOp c, WellTyped 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 :: forall aop inp m n s t. (ArithOp aop n m, WellTyped (ArithRes aop n m), inp ~ (n ': (m ': s)), MonadReader InstrCallStack t, MonadError TCError t) => Instr inp (ArithRes aop n m ': s) -> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)

Helper function to construct instructions for binary arithmetic operations.

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

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

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

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

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

Helper function to construct instructions for unary arithmetic operations.

unaryArithImplAnnotated :: (WellTyped (UnaryArithRes aop n), inp ~ (n ': s), Monad t, n ~ UnaryArithRes aop n) => Instr inp (UnaryArithRes aop n ': s) -> HST inp -> VarAnn -> t (SomeInstr inp)

Helper function to construct instructions for unary arithmetic operations that should preserve annotations.

withCompareableCheck :: forall a m v ts. (SingI ts, MonadReader InstrCallStack m, MonadError TCError m) => Sing a -> ExpandedInstr -> HST ts -> (Comparable a => v) -> m v