Safe Haskell	None
Language	Haskell2010

Michelson.TypeCheck.Helpers

Synopsis

onLeft :: Either a c -> (a -> b) -> Either b c
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 -> TypeCheckInstr (SomeInstr 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)
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

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

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

hstToTs :: HST st -> [T] Source #

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

lengthHST :: HST xs -> Natural Source #

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 -> TypeCheckInstr (SomeInstr inp) Source #

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 #

sizeImpl :: (SizeOp c, inp ~ (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 binary arithmetic operations.

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 #