| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Michelson.TypeCheck.Helpers
Synopsis
- deriveSpecialVN :: VarAnn -> FieldAnn -> VarAnn -> VarAnn
- deriveSpecialFNs :: FieldAnn -> FieldAnn -> VarAnn -> VarAnn -> (VarAnn, FieldAnn, FieldAnn)
- deriveVN :: VarAnn -> VarAnn -> VarAnn
- deriveNsOr :: Notes ('TOr a b) -> VarAnn -> (Notes a, Notes b, VarAnn, VarAnn)
- deriveNsOption :: Notes ('TOption a) -> VarAnn -> (Notes a, VarAnn)
- 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)
- hstToTs :: HST st -> [T]
- eqHST :: forall as bs. (Typeable as, Typeable bs) => HST as -> HST bs -> Either TCTypeError (as :~: bs)
- eqHST1 :: forall t st. (Typeable st, WellTyped t) => HST st -> Either TCTypeError (st :~: '[t])
- lengthHST :: HST xs -> Natural
- ensureDistinctAsc :: (Ord b, Show a) => (a -> b) -> [a] -> Either Text [a]
- eqType :: forall (a :: T) (b :: T). Each '[KnownT] [a, b] => Either TCTypeError (a :~: b)
- onTypeCheckInstrAnnErr :: (MonadReader InstrCallStack m, MonadError TCError m, Typeable 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. Typeable inp => TcInstrHandler -> [ExpandedOp] -> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
- typeCheckImplStripped :: forall inp. Typeable inp => TcInstrHandler -> [ExpandedOp] -> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
- matchTypes :: forall t1 t2. Each '[KnownT] [t1, t2] => Notes t1 -> Notes t2 -> Either TCTypeError (t1 :~: t2, Notes t1)
- memImpl :: forall c memKey rs inp m. (MemOp c, KnownT (MemOpKey c), inp ~ (memKey ': (c ': rs)), MonadReader InstrCallStack m, MonadError TCError m) => Notes (MemOpKey c) -> HST inp -> VarAnn -> m (SomeInstr inp)
- getImpl :: forall c getKey rs inp m. (GetOp c, KnownT (GetOpKey c), WellTyped (GetOpVal c), inp ~ (getKey ': (c ': 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, KnownT (UpdOpKey c), KnownT (UpdOpParams c), inp ~ (updKey ': (updParams ': (c ': rs))), MonadReader InstrCallStack m, MonadError TCError m) => Notes (UpdOpKey c) -> HST inp -> Notes (UpdOpParams c) -> VarAnn -> m (SomeInstr inp)
- sliceImpl :: (SliceOp c, Typeable 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, Typeable (ArithRes aop n m ': s), 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)
- addImpl :: forall a b inp rs m. (Typeable rs, Each '[KnownT] [a, b], inp ~ (a ': (b ': 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. (Typeable rs, Each '[KnownT] [a, b], inp ~ (a ': (b ': 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. (Typeable rs, Each '[KnownT] [a, b], inp ~ (a ': (b ': 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. (Typeable rs, Each '[KnownT] [a, b], inp ~ (a ': (b ': rs)), MonadReader InstrCallStack m, MonadError TCError m) => Sing a -> Sing b -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
- unaryArithImpl :: (Typeable (UnaryArithRes aop n ': s), WellTyped (UnaryArithRes aop n), inp ~ (n ': s), Monad t) => Instr inp (UnaryArithRes aop n ': s) -> HST inp -> VarAnn -> t (SomeInstr inp)
- unaryArithImplAnnotated :: (Typeable (UnaryArithRes aop n ': s), 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)
- withCompareableCheck :: forall a m v ts. (Typeable ts, MonadReader InstrCallStack m, MonadError TCError m) => Sing a -> ExpandedInstr -> HST ts -> (Comparable a => v) -> m v
Documentation
deriveSpecialVN :: VarAnn -> FieldAnn -> VarAnn -> VarAnn Source #
Function which derives special annotations for CDR / CAR instructions.
deriveSpecialFNs :: FieldAnn -> FieldAnn -> VarAnn -> VarAnn -> (VarAnn, FieldAnn, FieldAnn) Source #
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 Source #
Append suffix to variable annotation (if it's not empty)
deriveNsOr :: Notes ('TOr a b) -> VarAnn -> (Notes a, Notes b, VarAnn, VarAnn) Source #
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) Source #
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) Source #
convergeHST :: HST ts -> HST ts -> Either AnnConvergeError (HST ts) Source #
Combine annotations from two given stack types
eqHST :: forall as bs. (Typeable as, Typeable bs) => HST as -> HST bs -> Either TCTypeError (as :~: bs) Source #
Check whether the given stack types are equal.
eqHST1 :: forall t st. (Typeable st, WellTyped t) => HST st -> Either TCTypeError (st :~: '[t]) Source #
Check whether the given stack has size 1 and its only element matches the
given type. This function is a specialized version of eqHST.
ensureDistinctAsc :: (Ord b, Show a) => (a -> b) -> [a] -> Either Text [a] Source #
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 '[KnownT] [a, b] => Either TCTypeError (a :~: b) Source #
Function eqType is a simple wrapper around Data.Typeable.eqT suited
for use within Either TCTypeError a applicative.
onTypeCheckInstrAnnErr :: (MonadReader InstrCallStack m, MonadError TCError m, Typeable ts) => ExpandedInstr -> HST ts -> Maybe TypeContext -> Either AnnConvergeError a -> m a Source #
onTypeCheckInstrErr :: (MonadReader InstrCallStack m, MonadError TCError m) => ExpandedInstr -> SomeHST -> Maybe TypeContext -> Either TCTypeError a -> m a Source #
onScopeCheckInstrErr :: forall (t :: T) m a. (MonadReader InstrCallStack m, MonadError TCError m, SingI t) => ExpandedInstr -> SomeHST -> Maybe TypeContext -> Either BadTypeForScope a -> m a Source #
typeCheckInstrErr :: (MonadReader InstrCallStack m, MonadError TCError m) => ExpandedInstr -> SomeHST -> Maybe TypeContext -> m a Source #
typeCheckInstrErr' :: (MonadReader InstrCallStack m, MonadError TCError m) => ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a Source #
typeCheckImpl :: forall inp. Typeable inp => TcInstrHandler -> [ExpandedOp] -> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) Source #
typeCheckImplStripped :: forall inp. Typeable inp => TcInstrHandler -> [ExpandedOp] -> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp) Source #
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 '[KnownT] [t1, t2] => Notes t1 -> Notes t2 -> Either TCTypeError (t1 :~: t2, Notes t1) Source #
Check whether given types are structurally equal and annotations converge.
memImpl :: forall c memKey rs inp m. (MemOp c, KnownT (MemOpKey c), inp ~ (memKey ': (c ': rs)), MonadReader InstrCallStack m, MonadError TCError m) => Notes (MemOpKey c) -> HST inp -> VarAnn -> m (SomeInstr inp) Source #
Generic implementation for MEMeration
getImpl :: forall c getKey rs inp m. (GetOp c, KnownT (GetOpKey c), WellTyped (GetOpVal c), inp ~ (getKey ': (c ': rs)), MonadReader InstrCallStack m, MonadError TCError m) => Notes (GetOpKey c) -> HST inp -> Notes (GetOpVal c) -> VarAnn -> m (SomeInstr inp) Source #
updImpl :: forall c updKey updParams rs inp m. (UpdOp c, KnownT (UpdOpKey c), KnownT (UpdOpParams c), inp ~ (updKey ': (updParams ': (c ': rs))), MonadReader InstrCallStack m, MonadError TCError m) => Notes (UpdOpKey c) -> HST inp -> Notes (UpdOpParams c) -> VarAnn -> m (SomeInstr inp) Source #
sliceImpl :: (SliceOp c, Typeable c, inp ~ ('TNat ': ('TNat ': (c ': rs))), Monad m) => HST inp -> VarAnn -> m (SomeInstr inp) Source #
concatImpl :: (ConcatOp c, inp ~ (c ': (c ': rs)), WellTyped c, MonadReader InstrCallStack m, MonadError TCError m) => HST inp -> VarAnn -> m (SomeInstr inp) Source #
concatImpl' :: (ConcatOp c, WellTyped c, inp ~ ('TList c ': rs), Monad m) => HST inp -> VarAnn -> m (SomeInstr inp) Source #
arithImpl :: forall aop inp m n s t. (ArithOp aop n m, Typeable (ArithRes aop n m ': s), 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) Source #
Helper function to construct instructions for binary arithmetic operations.
addImpl :: forall a b inp rs m. (Typeable rs, Each '[KnownT] [a, b], inp ~ (a ': (b ': rs)), MonadReader InstrCallStack m, MonadError TCError m) => Sing a -> Sing b -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp) Source #
subImpl :: forall a b inp rs m. (Typeable rs, Each '[KnownT] [a, b], inp ~ (a ': (b ': rs)), MonadReader InstrCallStack m, MonadError TCError m) => Sing a -> Sing b -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp) Source #
mulImpl :: forall a b inp rs m. (Typeable rs, Each '[KnownT] [a, b], inp ~ (a ': (b ': rs)), MonadReader InstrCallStack m, MonadError TCError m) => Sing a -> Sing b -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp) Source #
edivImpl :: forall a b inp rs m. (Typeable rs, Each '[KnownT] [a, b], inp ~ (a ': (b ': rs)), MonadReader InstrCallStack m, MonadError TCError m) => Sing a -> Sing b -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp) Source #
unaryArithImpl :: (Typeable (UnaryArithRes aop n ': s), WellTyped (UnaryArithRes aop n), inp ~ (n ': s), Monad t) => Instr inp (UnaryArithRes aop n ': s) -> HST inp -> VarAnn -> t (SomeInstr inp) Source #
Helper function to construct instructions for unary arithmetic operations.
unaryArithImplAnnotated :: (Typeable (UnaryArithRes aop n ': s), 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) Source #
Helper function to construct instructions for unary arithmetic operations that should preserve annotations.
withCompareableCheck :: forall a m v ts. (Typeable ts, MonadReader InstrCallStack m, MonadError TCError m) => Sing a -> ExpandedInstr -> HST ts -> (Comparable a => v) -> m v Source #