Morley.Michelson.TypeCheck.Helpers

Documentation

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.

lengthHST :: HST xs -> Natural

ensureDistinctAsc :: (Ord b, Buildable 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.

onTypeCheckInstrErr :: (MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) => InstrAbstract [] op -> SomeHST -> Maybe TypeContext -> Either TcTypeError a -> m a

onScopeCheckInstrErr :: forall (t :: T) op m a. (MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m, SingI t) => InstrAbstract [] op -> SomeHST -> Maybe TypeContext -> Either BadTypeForScope a -> m a

typeCheckInstrErr :: (MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) => InstrAbstract [] op -> SomeHST -> Maybe TypeContext -> m a

typeCheckInstrErr' :: (MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) => InstrAbstract [] op -> SomeHST -> Maybe TypeContext -> TcTypeError -> m a

typeCheckImpl :: forall op. IsInstrOp op => TcInstrBase op -> TcInstr op [op]

typeCheckImplStripped :: IsInstrOp op => TcInstrBase op -> TcInstr op [op]

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

mapSeq :: (SomeTcInstr inp -> SomeTcInstr inp') -> TypeCheckedSeq op inp -> TypeCheckedSeq op inp'

wrapWithLoc :: ErrorSrcPos -> TypeCheckedSeq op inp -> TypeCheckedSeq op inp

memImpl :: forall c memKey rs inp m op. (MemOp c, SingI (MemOpKey c), inp ~ (memKey : (c : rs)), SingI rs, MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) => HST inp -> VarAnn -> m (SomeTcInstr inp)

Generic implementation for MEMeration

getImpl :: forall c getKey rs inp m op. (GetOp c, SingI (GetOpKey c), WellTyped (GetOpVal c), inp ~ (getKey : (c : rs)), SingI rs, MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) => HST inp -> SingT (GetOpVal c) -> VarAnn -> m (SomeTcInstr inp)

updImpl :: forall c updKey updParams rs inp m op. (UpdOp c, SingI (UpdOpKey c), SingI (UpdOpParams c), SingI rs, inp ~ (updKey : (updParams : (c : rs))), MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) => HST inp -> VarAnn -> m (SomeTcInstr inp)

getUpdImpl :: forall c updKey updParams rs inp m op. (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 TypeCheckInstrEnv m, MonadError (TcError' op) m) => HST inp -> VarAnn -> m (SomeTcInstr inp)

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

concatImpl :: (ConcatOp c, inp ~ (c ': (c ': rs)), WellTyped c, MonadReader TypeCheckInstrEnv m) => HST inp -> VarAnn -> m (SomeTcInstr inp)

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

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

arithImpl :: forall aop inp m n s t op. (WellTyped (ArithRes aop n m), inp ~ (n ': (m ': s)), MonadReader TypeCheckInstrEnv t) => (Anns '[VarAnn] -> Instr inp (ArithRes aop n m ': s)) -> HST inp -> VarAnn -> InstrAbstract [] op -> t (SomeTcInstr inp)

Helper function to construct instructions for binary arithmetic operations.

addImpl :: forall a b inp rs m op. (Each '[SingI] [a, b], inp ~ (a ': (b ': rs)), SingI rs, MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) => Sing a -> Sing b -> HST inp -> VarAnn -> InstrAbstract [] op -> m (SomeTcInstr inp)

subImpl :: forall a b inp rs m op. (Each '[SingI] [a, b], inp ~ (a ': (b ': rs)), SingI rs, MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) => Sing a -> Sing b -> HST inp -> VarAnn -> InstrAbstract [] op -> m (SomeTcInstr inp)

mulImpl :: forall a b inp rs m op. (Each '[SingI] [a, b], inp ~ (a ': (b ': rs)), SingI rs, MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) => Sing a -> Sing b -> HST inp -> VarAnn -> InstrAbstract [] op -> m (SomeTcInstr inp)

edivImpl :: forall a b inp rs m op. (SingI rs, Each '[SingI] [a, b], inp ~ (a ': (b ': rs)), MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) => Sing a -> Sing b -> HST inp -> VarAnn -> InstrAbstract [] op -> m (SomeTcInstr inp)

unaryArithImpl :: (WellTyped (UnaryArithRes aop n), inp ~ (n ': s), Monad t) => Instr inp (UnaryArithRes aop n ': s) -> HST inp -> t (SomeTcInstr 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 -> t (SomeTcInstr inp)

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

withCompareableCheck :: forall a m v ts op. (SingI ts, MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) => Sing a -> InstrAbstract [] op -> HST ts -> (Comparable a => v) -> m v

checkContractDeprecations :: forall cp st op. Contract cp st -> Either (TcError' op) ()

checkSingDeprecations :: SingT t -> Either (TcError' op) ()