module Morley.Michelson.TypeCheck.Helpers
( hstToTs
, eqHST
, eqHST1
, lengthHST
, ensureDistinctAsc
, handleError
, eqType
, onTypeCheckInstrErr
, onScopeCheckInstrErr
, typeCheckInstrErr
, typeCheckInstrErr'
, typeCheckImpl
, typeCheckImplStripped
, mapSeq
, wrapWithLoc
, memImpl
, getImpl
, updImpl
, getUpdImpl
, sliceImpl
, concatImpl
, concatImpl'
, sizeImpl
, arithImpl
, addImpl
, subImpl
, mulImpl
, edivImpl
, unaryArithImpl
, unaryArithImplAnnotated
, withCompareableCheck
, checkContractDeprecations
, checkSingDeprecations
) where
import Prelude hiding (EQ, GT, LT)
import Control.Monad.Except (MonadError, catchError, liftEither, throwError)
import Data.Constraint (Dict(..), withDict)
import Data.Default (def)
import Data.Generics (listify)
import Data.Singletons (Sing, SingI(sing), demote, fromSing)
import Data.Singletons.Decide ((:~:)(Refl))
import Fmt (Buildable, (+|), (|+))
import Morley.Michelson.ErrorPos (ErrorSrcPos)
import Morley.Michelson.TypeCheck.Error (TcError'(..), TcTypeError(..), TypeContext(..))
import Morley.Michelson.TypeCheck.TypeCheck
import Morley.Michelson.TypeCheck.TypeCheckedSeq (IllTypedInstr(..), TypeCheckedSeq(..))
import Morley.Michelson.TypeCheck.Types
import Morley.Michelson.Typed
(BadTypeForScope(..), CommentType(StackTypeComment), Comparable, Contract, Contract'(..),
ExtInstr(COMMENT_ITEM), Instr(..), SingT(..), T(..), WellTyped, getComparableProofS, requireEq)
import Morley.Michelson.Typed.Annotation
import Morley.Michelson.Typed.Arith (Add, ArithOp(..), EDiv, Mul, Sub, UnaryArithOp(..))
import Morley.Michelson.Typed.Polymorphic
(ConcatOp, EDivOp(..), GetOp(..), MemOp(..), SizeOp, SliceOp, UpdOp(..))
import Morley.Michelson.Untyped qualified as Un
import Morley.Michelson.Untyped.Annotation (VarAnn)
import Morley.Util.MismatchError
import Morley.Util.Sing (eqI)
hstToTs :: HST st -> [T]
hstToTs :: forall (st :: [T]). HST st -> [T]
hstToTs = \case
HST st
SNil -> []
(SingT x
ts, Dict (WellTyped x)
_) ::& HST xs
hst -> Sing x -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
SingT x
ts T -> [T] -> [T]
forall a. a -> [a] -> [a]
: HST xs -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST xs
hst
eqHST
:: forall as bs. (SingI as, SingI bs)
=> HST as -> HST bs -> Either TcTypeError (as :~: bs)
eqHST :: forall (as :: [T]) (bs :: [T]).
(SingI as, SingI bs) =>
HST as -> HST bs -> Either TcTypeError (as :~: bs)
eqHST (HST as
hst :: HST xs) (HST bs
hst' :: HST ys) = do
case forall (a :: [T]) (b :: [T]).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @as @bs of
Maybe (as :~: bs)
Nothing -> TcTypeError -> Either TcTypeError (as :~: bs)
forall a b. a -> Either a b
Left (TcTypeError -> Either TcTypeError (as :~: bs))
-> TcTypeError -> Either TcTypeError (as :~: bs)
forall a b. (a -> b) -> a -> b
$ MismatchError [T] -> TcTypeError
StackEqError MkMismatchError :: forall a. a -> a -> MismatchError a
MkMismatchError {meActual :: [T]
meActual = HST as -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST as
hst, meExpected :: [T]
meExpected = HST bs -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST bs
hst'}
Just as :~: bs
Refl -> (as :~: as) -> Either TcTypeError (as :~: as)
forall a b. b -> Either a b
Right as :~: as
forall {k} (a :: k). a :~: a
Refl
eqHST1
:: forall t st. (SingI st, WellTyped t)
=> HST st -> Either TcTypeError (st :~: '[t])
eqHST1 :: forall (t :: T) (st :: [T]).
(SingI st, WellTyped t) =>
HST st -> Either TcTypeError (st :~: '[t])
eqHST1 HST st
hst = do
let hst' :: HST '[t]
hst' = forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @t Sing t -> HST '[] -> HST '[t]
forall (x :: T) (xs :: [T]).
(WellTyped x, SingI xs) =>
Sing x -> HST xs -> HST (x : xs)
-:& HST '[]
SNil
case forall (a :: [T]) (b :: [T]).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @'[t] @st of
Maybe ('[t] :~: st)
Nothing -> TcTypeError -> Either TcTypeError (st :~: '[t])
forall a b. a -> Either a b
Left (TcTypeError -> Either TcTypeError (st :~: '[t]))
-> TcTypeError -> Either TcTypeError (st :~: '[t])
forall a b. (a -> b) -> a -> b
$ MismatchError [T] -> TcTypeError
StackEqError MkMismatchError :: forall a. a -> a -> MismatchError a
MkMismatchError {meActual :: [T]
meActual = HST st -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST st
hst, meExpected :: [T]
meExpected = HST '[t] -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST '[t]
hst'}
Just '[t] :~: st
Refl -> (st :~: st) -> Either TcTypeError (st :~: st)
forall a b. b -> Either a b
Right st :~: st
forall {k} (a :: k). a :~: a
Refl
lengthHST :: HST xs -> Natural
lengthHST :: forall (xs :: [T]). HST xs -> Natural
lengthHST ((SingT x, Dict (WellTyped x))
_ ::& HST xs
xs) = Natural
1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ HST xs -> Natural
forall (xs :: [T]). HST xs -> Natural
lengthHST HST xs
xs
lengthHST HST xs
SNil = Natural
0
ensureDistinctAsc :: (Ord b, Buildable a) => (a -> b) -> [a] -> Either Text [a]
ensureDistinctAsc :: forall b a.
(Ord b, Buildable a) =>
(a -> b) -> [a] -> Either Text [a]
ensureDistinctAsc a -> b
toCmp = \case
(a
e1 : a
e2 : [a]
l) ->
if a -> b
toCmp a
e1 b -> b -> Bool
forall a. Ord a => a -> a -> Bool
< a -> b
toCmp a
e2
then (a
e1 a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> [a]) -> Either Text [a] -> Either Text [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> b) -> [a] -> Either Text [a]
forall b a.
(Ord b, Buildable a) =>
(a -> b) -> [a] -> Either Text [a]
ensureDistinctAsc a -> b
toCmp (a
e2 a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
l)
else Text -> Either Text [a]
forall a b. a -> Either a b
Left (Text -> Either Text [a]) -> Text -> Either Text [a]
forall a b. (a -> b) -> a -> b
$ Builder
"Entries are unordered (" Builder -> Builder -> Text
forall b. FromBuilder b => Builder -> Builder -> b
+| a
e1 a -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
" >= " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| a
e2 a -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
")"
[a]
l -> [a] -> Either Text [a]
forall a b. b -> Either a b
Right [a]
l
handleError :: MonadError e m => (e -> m a) -> m a -> m a
handleError :: forall e (m :: * -> *) a.
MonadError e m =>
(e -> m a) -> m a -> m a
handleError = (m a -> (e -> m a) -> m a) -> (e -> m a) -> m a -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip m a -> (e -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError
eqType
:: forall (a :: T) (b :: T). (Each '[SingI] [a, b])
=> Either TcTypeError (a :~: b)
eqType :: forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TcTypeError (a :~: b)
eqType =
forall (a :: T) (b :: T) (m :: * -> *).
(SingI a, SingI b, Monad m) =>
(forall x. MismatchError T -> m x) -> m (a :~: b)
requireEq @a @b ((forall x. MismatchError T -> Either TcTypeError x)
-> Either TcTypeError (a :~: b))
-> (forall x. MismatchError T -> Either TcTypeError x)
-> Either TcTypeError (a :~: b)
forall a b. (a -> b) -> a -> b
$ TcTypeError -> Either TcTypeError x
forall a b. a -> Either a b
Left (TcTypeError -> Either TcTypeError x)
-> (MismatchError T -> TcTypeError)
-> MismatchError T
-> Either TcTypeError x
forall a b c. SuperComposition a b c => a -> b -> c
... MismatchError T -> TcTypeError
TypeEqError
onTypeCheckInstrErr
:: (MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m)
=> Un.InstrAbstract op -> SomeHST -> Maybe TypeContext
-> Either TcTypeError a -> m a
onTypeCheckInstrErr :: forall (m :: * -> *) op a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) =>
InstrAbstract op
-> SomeHST -> Maybe TypeContext -> Either TcTypeError a -> m a
onTypeCheckInstrErr InstrAbstract op
instr SomeHST
hst Maybe TypeContext
mContext Either TcTypeError a
ei = do
(TcTypeError -> m a) -> (a -> m a) -> Either TcTypeError a -> m a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (InstrAbstract op
-> SomeHST -> Maybe TypeContext -> TcTypeError -> m a
forall (m :: * -> *) op a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) =>
InstrAbstract op
-> SomeHST -> Maybe TypeContext -> TcTypeError -> m a
typeCheckInstrErr' InstrAbstract op
instr SomeHST
hst Maybe TypeContext
mContext) a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Either TcTypeError a
ei
onScopeCheckInstrErr
:: forall (t :: T) op m a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m, SingI t)
=> Un.InstrAbstract op -> SomeHST -> Maybe TypeContext
-> Either BadTypeForScope 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
onScopeCheckInstrErr InstrAbstract op
instr SomeHST
hst Maybe TypeContext
mContext = \case
Right a
a -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
Left BadTypeForScope
e -> do
ErrorSrcPos
pos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos -> m ErrorSrcPos
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos
TcError' op -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TcError' op -> m a) -> TcError' op -> m a
forall a b. (a -> b) -> a -> b
$ InstrAbstract op
-> SomeHST
-> ErrorSrcPos
-> Maybe TypeContext
-> Maybe TcTypeError
-> TcError' op
forall op.
InstrAbstract op
-> SomeHST
-> ErrorSrcPos
-> Maybe TypeContext
-> Maybe TcTypeError
-> TcError' op
TcFailedOnInstr InstrAbstract op
instr SomeHST
hst ErrorSrcPos
pos Maybe TypeContext
mContext (Maybe TcTypeError -> TcError' op)
-> Maybe TcTypeError -> TcError' op
forall a b. (a -> b) -> a -> b
$
TcTypeError -> Maybe TcTypeError
forall a. a -> Maybe a
Just (TcTypeError -> Maybe TcTypeError)
-> TcTypeError -> Maybe TcTypeError
forall a b. (a -> b) -> a -> b
$ T -> BadTypeForScope -> TcTypeError
UnsupportedTypeForScope (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @t) BadTypeForScope
e
typeCheckInstrErr
:: (MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m)
=> Un.InstrAbstract op -> SomeHST -> Maybe TypeContext
-> m a
typeCheckInstrErr :: forall (m :: * -> *) op a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) =>
InstrAbstract op -> SomeHST -> Maybe TypeContext -> m a
typeCheckInstrErr InstrAbstract op
instr SomeHST
hst Maybe TypeContext
mContext = do
ErrorSrcPos
pos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos -> m ErrorSrcPos
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos
TcError' op -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TcError' op -> m a) -> TcError' op -> m a
forall a b. (a -> b) -> a -> b
$ InstrAbstract op
-> SomeHST
-> ErrorSrcPos
-> Maybe TypeContext
-> Maybe TcTypeError
-> TcError' op
forall op.
InstrAbstract op
-> SomeHST
-> ErrorSrcPos
-> Maybe TypeContext
-> Maybe TcTypeError
-> TcError' op
TcFailedOnInstr InstrAbstract op
instr SomeHST
hst ErrorSrcPos
pos Maybe TypeContext
mContext Maybe TcTypeError
forall a. Maybe a
Nothing
typeCheckInstrErr'
:: (MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m)
=> Un.InstrAbstract op -> SomeHST -> Maybe TypeContext
-> TcTypeError -> m a
typeCheckInstrErr' :: forall (m :: * -> *) op a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) =>
InstrAbstract op
-> SomeHST -> Maybe TypeContext -> TcTypeError -> m a
typeCheckInstrErr' InstrAbstract op
instr SomeHST
hst Maybe TypeContext
mContext TcTypeError
err = do
ErrorSrcPos
pos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos -> m ErrorSrcPos
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos
TcError' op -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TcError' op -> m a) -> TcError' op -> m a
forall a b. (a -> b) -> a -> b
$ InstrAbstract op
-> SomeHST
-> ErrorSrcPos
-> Maybe TypeContext
-> Maybe TcTypeError
-> TcError' op
forall op.
InstrAbstract op
-> SomeHST
-> ErrorSrcPos
-> Maybe TypeContext
-> Maybe TcTypeError
-> TcError' op
TcFailedOnInstr InstrAbstract op
instr SomeHST
hst ErrorSrcPos
pos Maybe TypeContext
mContext (TcTypeError -> Maybe TcTypeError
forall a. a -> Maybe a
Just TcTypeError
err)
withCompareableCheck
:: forall a m v ts op. (SingI ts, MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m)
=> Sing a
-> Un.InstrAbstract op
-> HST ts
-> (Comparable a => v)
-> m v
withCompareableCheck :: forall (a :: T) (m :: * -> *) v (ts :: [T]) op.
(SingI ts, MonadReader TypeCheckInstrEnv m,
MonadError (TcError' op) m) =>
Sing a -> InstrAbstract op -> HST ts -> (Comparable a => v) -> m v
withCompareableCheck Sing a
sng InstrAbstract op
instr HST ts
i Comparable a => v
act = case Sing a -> Maybe (Dict (Comparable a))
forall (a :: T). Sing a -> Maybe (Dict (Comparable a))
getComparableProofS Sing a
sng of
Just d :: Dict (Comparable a)
d@Dict (Comparable a)
Dict -> v -> m v
forall (f :: * -> *) a. Applicative f => a -> f a
pure (v -> m v) -> v -> m v
forall a b. (a -> b) -> a -> b
$ Dict (Comparable a) -> (Comparable a => v) -> v
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict Dict (Comparable a)
d Comparable a => v
act
Maybe (Dict (Comparable a))
Nothing -> InstrAbstract op -> SomeHST -> Maybe TypeContext -> m v
forall (m :: * -> *) op a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) =>
InstrAbstract op -> SomeHST -> Maybe TypeContext -> m a
typeCheckInstrErr InstrAbstract op
instr (HST ts -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST ts
i) (Maybe TypeContext -> m v) -> Maybe TypeContext -> m v
forall a b. (a -> b) -> a -> b
$ TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ComparisonArguments
typeCheckImplNoLastTypeComment
:: IsInstrOp op
=> TcInstrBase op
-> TcInstr op [op]
TcInstrBase op
_ [] HST inp
inputStack
= TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTcInstr inp -> TypeCheckedSeq op inp
forall op (inp :: [T]). SomeTcInstr inp -> TypeCheckedSeq op inp
WellTypedSeq (HST inp
inputStack HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop Instr inp inp -> HST inp -> SomeTcInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: HST inp
inputStack))
typeCheckImplNoLastTypeComment TcInstrBase op
tcOp [op
op] HST inp
inputStack = do
op
-> HST inp
-> MultiReaderT
'[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
Identity
(TypeCheckedSeq op inp)
TcInstrBase op
tcOp op
op HST inp
inputStack
ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
-> (TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp))
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (SomeTcInstr inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(SomeTcInstr inp))
-> TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall (f :: * -> *) (inp :: [T]) (inp' :: [T]) op.
Applicative f =>
(SomeTcInstr inp -> f (SomeTcInstr inp'))
-> TypeCheckedSeq op inp -> f (TypeCheckedSeq op inp')
mapMSeq SomeTcInstr inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(SomeTcInstr inp)
forall (inp :: [T]) op.
SomeTcInstr inp -> TypeCheckInstrNoExcept op (SomeTcInstr inp)
prependStackTypeComment
typeCheckImplNoLastTypeComment TcInstrBase op
tcOp (op
op : [op]
ops) HST inp
inputStack = do
TypeCheckedSeq op inp
done <- op
-> HST inp
-> MultiReaderT
'[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
Identity
(TypeCheckedSeq op inp)
TcInstrBase op
tcOp op
op HST inp
inputStack
ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
-> (TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp))
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (SomeTcInstr inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(SomeTcInstr inp))
-> TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall (f :: * -> *) (inp :: [T]) (inp' :: [T]) op.
Applicative f =>
(SomeTcInstr inp -> f (SomeTcInstr inp'))
-> TypeCheckedSeq op inp -> f (TypeCheckedSeq op inp')
mapMSeq SomeTcInstr inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(SomeTcInstr inp)
forall (inp :: [T]) op.
SomeTcInstr inp -> TypeCheckInstrNoExcept op (SomeTcInstr inp)
prependStackTypeComment
TcInstrBase op
-> TypeCheckedSeq op inp
-> [op]
-> MultiReaderT
'[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
Identity
(TypeCheckedSeq op inp)
forall op (inp :: [T]).
IsInstrOp op =>
TcInstrBase op
-> TypeCheckedSeq op inp
-> [op]
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
continueTypeChecking TcInstrBase op
tcOp TypeCheckedSeq op inp
done [op]
ops
continueTypeChecking
:: forall op inp. (IsInstrOp op)
=> TcInstrBase op
-> TypeCheckedSeq op inp
-> [op]
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
continueTypeChecking :: forall op (inp :: [T]).
IsInstrOp op =>
TcInstrBase op
-> TypeCheckedSeq op inp
-> [op]
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
continueTypeChecking TcInstrBase op
tcOp TypeCheckedSeq op inp
done [op]
rest = case TypeCheckedSeq op inp
done of
WellTypedSeq SomeTcInstr inp
instr -> SomeTcInstr inp
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
handleFirst SomeTcInstr inp
instr
MixedSeq SomeTcInstr inp
i TcError' op
e [IllTypedInstr op]
left -> TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTcInstr inp
-> TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
forall op (inp :: [T]).
SomeTcInstr inp
-> TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
MixedSeq SomeTcInstr inp
i TcError' op
e ([IllTypedInstr op]
left [IllTypedInstr op] -> [IllTypedInstr op] -> [IllTypedInstr op]
forall a. Semigroup a => a -> a -> a
<> (op -> IllTypedInstr op) -> [op] -> [IllTypedInstr op]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map op -> IllTypedInstr op
forall op. op -> IllTypedInstr op
NonTypedInstr [op]
rest))
IllTypedSeq TcError' op
e [IllTypedInstr op]
left -> TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
forall op (inp :: [T]).
TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
IllTypedSeq TcError' op
e ([IllTypedInstr op]
left [IllTypedInstr op] -> [IllTypedInstr op] -> [IllTypedInstr op]
forall a. Semigroup a => a -> a -> a
<> (op -> IllTypedInstr op) -> [op] -> [IllTypedInstr op]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map op -> IllTypedInstr op
forall op. op -> IllTypedInstr op
NonTypedInstr [op]
rest))
where
handleFirst :: SomeTcInstr inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
handleFirst :: SomeTcInstr inp
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
handleFirst packedInstr :: SomeTcInstr inp
packedInstr@(HST inp
inputStack :/ SomeTcInstrOut inp
instrAndOutputStack) = do
case SomeTcInstrOut inp
instrAndOutputStack of
Instr inp out
instr ::: HST out
outputStack -> do
TypeCheckedSeq op out
nextPiece <- TcInstrBase op -> TcInstr op [op]
forall op. IsInstrOp op => TcInstrBase op -> TcInstr op [op]
typeCheckImplNoLastTypeComment TcInstrBase op
tcOp [op]
rest HST out
outputStack
let combiner :: SomeTcInstr out -> SomeTcInstr inp
combiner = HST inp -> Instr inp out -> SomeTcInstr out -> SomeTcInstr inp
forall {inp :: [T]} {inp :: [T]}.
HST inp -> Instr inp inp -> SomeTcInstr inp -> SomeTcInstr inp
combine HST inp
inputStack Instr inp out
instr
TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure case TypeCheckedSeq op out
nextPiece of
WellTypedSeq SomeTcInstr out
nextInstr -> SomeTcInstr inp -> TypeCheckedSeq op inp
forall op (inp :: [T]). SomeTcInstr inp -> TypeCheckedSeq op inp
WellTypedSeq (SomeTcInstr out -> SomeTcInstr inp
combiner SomeTcInstr out
nextInstr)
MixedSeq SomeTcInstr out
nextInstr TcError' op
err [IllTypedInstr op]
left -> SomeTcInstr inp
-> TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
forall op (inp :: [T]).
SomeTcInstr inp
-> TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
MixedSeq (SomeTcInstr out -> SomeTcInstr inp
combiner SomeTcInstr out
nextInstr) TcError' op
err [IllTypedInstr op]
left
IllTypedSeq TcError' op
err [IllTypedInstr op]
left -> SomeTcInstr inp
-> TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
forall op (inp :: [T]).
SomeTcInstr inp
-> TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
MixedSeq SomeTcInstr inp
packedInstr TcError' op
err [IllTypedInstr op]
left
AnyOutInstr{} -> TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure case [op]
rest of
[] -> SomeTcInstr inp -> TypeCheckedSeq op inp
forall op (inp :: [T]). SomeTcInstr inp -> TypeCheckedSeq op inp
WellTypedSeq SomeTcInstr inp
packedInstr
op
op : [op]
ops -> (SomeTcInstr inp
-> TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
forall op (inp :: [T]).
SomeTcInstr inp
-> TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
MixedSeq
SomeTcInstr inp
packedInstr
(ErrorSrcPos -> NonEmpty op -> TcError' op
forall op. ErrorSrcPos -> NonEmpty op -> TcError' op
TcUnreachableCode (op -> ErrorSrcPos
extractOpPos op
op) (op
op op -> [op] -> NonEmpty op
forall a. a -> [a] -> NonEmpty a
:| [op]
ops))
((op -> IllTypedInstr op) -> [op] -> [IllTypedInstr op]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map op -> IllTypedInstr op
forall op. op -> IllTypedInstr op
NonTypedInstr [op]
ops))
combine :: HST inp -> Instr inp inp -> SomeTcInstr inp -> SomeTcInstr inp
combine HST inp
inp Instr inp inp
Nop (HST inp
_ :/ SomeTcInstrOut inp
nextPart) = HST inp
HST inp
inp HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ SomeTcInstrOut inp
nextPart
combine HST inp
inp Instr inp inp
i1 (HST inp
_ :/ SomeTcInstrOut inp
nextPart) = HST inp
inp HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ (forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeTcInstrOut inp -> SomeTcInstrOut inp
forall (inp :: [T]) (inp' :: [T]).
(forall (out :: [T]). Instr inp out -> Instr inp' out)
-> SomeTcInstrOut inp -> SomeTcInstrOut inp'
mapSomeInstrOut (Instr inp inp -> Instr inp out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr inp inp
i1) SomeTcInstrOut inp
nextPart
extractOpPos :: op -> ErrorSrcPos
extractOpPos :: op -> ErrorSrcPos
extractOpPos = ErrorSrcPos -> Maybe ErrorSrcPos -> ErrorSrcPos
forall a. a -> Maybe a -> a
fromMaybe ErrorSrcPos
forall a. Default a => a
def (Maybe ErrorSrcPos -> ErrorSrcPos)
-> (op -> Maybe ErrorSrcPos) -> op -> ErrorSrcPos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. op -> Maybe ErrorSrcPos
forall op. IsInstrOp op => op -> Maybe ErrorSrcPos
pickErrorSrcPos
typeCheckImplStripped
:: IsInstrOp op
=> TcInstrBase op
-> TcInstr op [op]
typeCheckImplStripped :: forall op. IsInstrOp op => TcInstrBase op -> TcInstr op [op]
typeCheckImplStripped TcInstrBase op
tcOp [] HST inp
inp
= TcInstrBase op -> TcInstr op [op]
forall op. IsInstrOp op => TcInstrBase op -> TcInstr op [op]
typeCheckImplNoLastTypeComment TcInstrBase op
tcOp [] HST inp
inp
typeCheckImplStripped TcInstrBase op
tcOp (op
op : [op]
ops) HST inp
inp = do
TypeCheckedSeq op inp
done <- op
-> HST inp
-> MultiReaderT
'[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
Identity
(TypeCheckedSeq op inp)
TcInstrBase op
tcOp op
op HST inp
inp
TcInstrBase op
-> TypeCheckedSeq op inp
-> [op]
-> MultiReaderT
'[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
Identity
(TypeCheckedSeq op inp)
forall op (inp :: [T]).
IsInstrOp op =>
TcInstrBase op
-> TypeCheckedSeq op inp
-> [op]
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
continueTypeChecking TcInstrBase op
tcOp TypeCheckedSeq op inp
done [op]
ops
typeCheckImpl
:: forall op. IsInstrOp op
=> TcInstrBase op
-> TcInstr op [op]
typeCheckImpl :: forall op. IsInstrOp op => TcInstrBase op -> TcInstr op [op]
typeCheckImpl TcInstrBase op
tcOp [op]
ops HST inp
inputStack = do
HST inp -> TypeCheckInstr op ()
forall (a :: [T]) op'. HST a -> TypeCheckInstr op' ()
checkBadTypes HST inp
inputStack ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
()
-> (ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
()
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp))
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall a b. a -> (a -> b) -> b
& (TcError' op -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> (() -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> TypeCheckInstr op ()
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
forall op a b.
(TcError' op -> TypeCheckInstrNoExcept op a)
-> (b -> TypeCheckInstrNoExcept op a)
-> TypeCheckInstr op b
-> TypeCheckInstrNoExcept op a
tcEither
(\TcError' op
err -> TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp))
-> TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall a b. (a -> b) -> a -> b
$ TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
forall op (inp :: [T]).
TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
IllTypedSeq TcError' op
err ([IllTypedInstr op] -> TypeCheckedSeq op inp)
-> [IllTypedInstr op] -> TypeCheckedSeq op inp
forall a b. (a -> b) -> a -> b
$ op -> IllTypedInstr op
forall op. op -> IllTypedInstr op
NonTypedInstr (op -> IllTypedInstr op) -> [op] -> [IllTypedInstr op]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [op]
ops)
(\()
_ -> TcInstrBase op -> TcInstr op [op]
forall op. IsInstrOp op => TcInstrBase op -> TcInstr op [op]
typeCheckImplNoLastTypeComment TcInstrBase op
tcOp [op]
ops HST inp
inputStack ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
-> (TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp))
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (SomeTcInstr inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(SomeTcInstr inp))
-> TypeCheckedSeq op inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op inp)
forall (f :: * -> *) (inp :: [T]) (inp' :: [T]) op.
Applicative f =>
(SomeTcInstr inp -> f (SomeTcInstr inp'))
-> TypeCheckedSeq op inp -> f (TypeCheckedSeq op inp')
mapMSeq SomeTcInstr inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(SomeTcInstr inp)
forall {f :: * -> *} {inp :: [T]}.
MultiReader
(MultiReaderDepth TypeCheckOptions (MultiReaderIso f))
TypeCheckOptions
f =>
SomeTcInstr inp -> f (SomeTcInstr inp)
appendTypeComment)
where
appendTypeComment :: SomeTcInstr inp -> f (SomeTcInstr inp)
appendTypeComment packedI :: SomeTcInstr inp
packedI@(HST inp
inp :/ SomeTcInstrOut inp
iAndOut) = do
Bool
verbose <- (TypeCheckOptions -> Bool) -> f Bool
forall (m :: * -> *) r a (n :: Peano).
MultiReader n r m =>
(r -> a) -> m a
asks' TypeCheckOptions -> Bool
tcVerbose
pure case (Bool
verbose, SomeTcInstrOut inp
iAndOut) of
(Bool
True, Instr inp out
i ::: HST out
out) -> HST inp
inp HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ Instr inp out -> Instr out out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr inp out
i (HST out -> Instr out out
forall (st :: [T]). HST st -> Instr st st
stackTypeComment HST out
out) Instr inp out -> HST out -> SomeTcInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: HST out
out
(Bool
True, AnyOutInstr forall (out :: [T]). Instr inp out
i) -> HST inp
inp HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ (forall (out :: [T]). Instr inp out) -> SomeTcInstrOut inp
forall (inp :: [T]).
(forall (out :: [T]). Instr inp out) -> SomeTcInstrOut inp
AnyOutInstr (Instr inp out -> Instr out out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr inp out
forall (out :: [T]). Instr inp out
i Instr out out
forall (inp :: [T]). Instr inp inp
noStackTypeComment)
(Bool, SomeTcInstrOut inp)
_ -> SomeTcInstr inp
packedI
checkBadTypes :: HST a -> TypeCheckInstr op' ()
checkBadTypes :: forall (a :: [T]) op'. HST a -> TypeCheckInstr op' ()
checkBadTypes HST a
x = do
Bool
isStrict <- (TypeCheckOptions -> Bool)
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op')
(ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity)))
Bool
forall (m :: * -> *) r a (n :: Peano).
MultiReader n r m =>
(r -> a) -> m a
asks' TypeCheckOptions -> Bool
tcStrict
Bool
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op')
(ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity)))
()
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op')
(ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity)))
()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isStrict (ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op')
(ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity)))
()
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op')
(ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity)))
())
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op')
(ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity)))
()
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op')
(ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity)))
()
forall a b. (a -> b) -> a -> b
$ HST a -> TypeCheckInstr op' ()
forall (a :: [T]) op'. HST a -> TypeCheckInstr op' ()
doCheckBadTypes HST a
x
doCheckBadTypes :: HST a -> TypeCheckInstr op' ()
doCheckBadTypes :: forall (a :: [T]) op'. HST a -> TypeCheckInstr op' ()
doCheckBadTypes = \case
HST a
SNil -> TypeCheckInstr op' ()
forall (f :: * -> *). Applicative f => f ()
pass
(SingT x
s, Dict (WellTyped x)
_) ::& HST xs
xs -> do
ReaderT
(TypeCheckEnv op')
(ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity))
()
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op')
(ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity)))
()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ReaderT
(TypeCheckEnv op')
(ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity))
()
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op')
(ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity)))
())
-> ReaderT
(TypeCheckEnv op')
(ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity))
()
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op')
(ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity)))
()
forall a b. (a -> b) -> a -> b
$ Either (TcError' op') ()
-> ReaderT
(TypeCheckEnv op')
(ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity))
()
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either (TcError' op') ()
-> ReaderT
(TypeCheckEnv op')
(ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity))
())
-> Either (TcError' op') ()
-> ReaderT
(TypeCheckEnv op')
(ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity))
()
forall a b. (a -> b) -> a -> b
$ SingT x -> Either (TcError' op') ()
forall (t :: T) op. SingT t -> Either (TcError' op) ()
checkSingDeprecations SingT x
s
HST xs -> TypeCheckInstr op' ()
forall (a :: [T]) op'. HST a -> TypeCheckInstr op' ()
doCheckBadTypes HST xs
xs
prependStackTypeComment
:: SomeTcInstr inp -> TypeCheckInstrNoExcept op (SomeTcInstr inp)
packedInstr :: SomeTcInstr inp
packedInstr@(HST inp
inp :/ SomeTcInstrOut inp
_) = do
Bool
verbose <- (TypeCheckOptions -> Bool)
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
Bool
forall (m :: * -> *) r a (n :: Peano).
MultiReader n r m =>
(r -> a) -> m a
asks' TypeCheckOptions -> Bool
tcVerbose
pure if Bool
verbose Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
&& (Bool -> Bool
forall a. Boolean a => a -> a
not (SomeTcInstr inp -> Bool
forall (inp :: [T]). SomeTcInstr inp -> Bool
isNop' SomeTcInstr inp
packedInstr))
then (forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeTcInstr inp -> SomeTcInstr inp
forall (inp :: [T]).
(forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeTcInstr inp -> SomeTcInstr inp
mapSomeInstr (Instr inp inp -> Instr inp out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq (HST inp -> Instr inp inp
forall (st :: [T]). HST st -> Instr st st
stackTypeComment HST inp
inp)) SomeTcInstr inp
packedInstr
else SomeTcInstr inp
packedInstr
isNop' :: SomeTcInstr inp -> Bool
isNop' :: forall (inp :: [T]). SomeTcInstr inp -> Bool
isNop' (HST inp
_ :/ Instr inp out
i ::: HST out
_) = Instr inp out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp out
i
isNop' (HST inp
_ :/ AnyOutInstr forall (out :: [T]). Instr inp out
i) = Instr inp Any -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp Any
forall (out :: [T]). Instr inp out
i
isNop :: Instr inp out -> Bool
isNop :: forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop (WithLoc ErrorSrcPos
_ Instr inp out
i) = Instr inp out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp out
i
isNop (Seq Instr inp b
i1 Instr b out
i2) = Instr inp b -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp b
i1 Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
&& Instr b out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr b out
i2
isNop (Nested Instr inp out
i) = Instr inp out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp out
i
isNop Instr inp out
Nop = Bool
True
isNop (Ext ExtInstr inp
_) = Bool
True
isNop Instr inp out
_ = Bool
False
mapMSeq
:: Applicative f
=> (SomeTcInstr inp -> f (SomeTcInstr inp'))
-> TypeCheckedSeq op inp
-> f (TypeCheckedSeq op inp')
mapMSeq :: forall (f :: * -> *) (inp :: [T]) (inp' :: [T]) op.
Applicative f =>
(SomeTcInstr inp -> f (SomeTcInstr inp'))
-> TypeCheckedSeq op inp -> f (TypeCheckedSeq op inp')
mapMSeq SomeTcInstr inp -> f (SomeTcInstr inp')
f TypeCheckedSeq op inp
v = case TypeCheckedSeq op inp
v of
WellTypedSeq SomeTcInstr inp
instr -> SomeTcInstr inp -> f (SomeTcInstr inp')
f SomeTcInstr inp
instr f (SomeTcInstr inp')
-> (SomeTcInstr inp' -> TypeCheckedSeq op inp')
-> f (TypeCheckedSeq op inp')
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> SomeTcInstr inp' -> TypeCheckedSeq op inp'
forall op (inp :: [T]). SomeTcInstr inp -> TypeCheckedSeq op inp
WellTypedSeq
MixedSeq SomeTcInstr inp
instr TcError' op
err [IllTypedInstr op]
tail' -> SomeTcInstr inp -> f (SomeTcInstr inp')
f SomeTcInstr inp
instr f (SomeTcInstr inp')
-> (SomeTcInstr inp' -> TypeCheckedSeq op inp')
-> f (TypeCheckedSeq op inp')
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \SomeTcInstr inp'
instr' -> SomeTcInstr inp'
-> TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp'
forall op (inp :: [T]).
SomeTcInstr inp
-> TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
MixedSeq SomeTcInstr inp'
instr' TcError' op
err [IllTypedInstr op]
tail'
IllTypedSeq TcError' op
err [IllTypedInstr op]
tail' -> TypeCheckedSeq op inp' -> f (TypeCheckedSeq op inp')
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq op inp' -> f (TypeCheckedSeq op inp'))
-> TypeCheckedSeq op inp' -> f (TypeCheckedSeq op inp')
forall a b. (a -> b) -> a -> b
$ TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp'
forall op (inp :: [T]).
TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
IllTypedSeq TcError' op
err [IllTypedInstr op]
tail'
mapSeq
:: (SomeTcInstr inp -> SomeTcInstr inp')
-> TypeCheckedSeq op inp
-> TypeCheckedSeq op inp'
mapSeq :: forall (inp :: [T]) (inp' :: [T]) op.
(SomeTcInstr inp -> SomeTcInstr inp')
-> TypeCheckedSeq op inp -> TypeCheckedSeq op inp'
mapSeq SomeTcInstr inp -> SomeTcInstr inp'
f = Identity (TypeCheckedSeq op inp') -> TypeCheckedSeq op inp'
forall a. Identity a -> a
runIdentity (Identity (TypeCheckedSeq op inp') -> TypeCheckedSeq op inp')
-> (TypeCheckedSeq op inp -> Identity (TypeCheckedSeq op inp'))
-> TypeCheckedSeq op inp
-> TypeCheckedSeq op inp'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SomeTcInstr inp -> Identity (SomeTcInstr inp'))
-> TypeCheckedSeq op inp -> Identity (TypeCheckedSeq op inp')
forall (f :: * -> *) (inp :: [T]) (inp' :: [T]) op.
Applicative f =>
(SomeTcInstr inp -> f (SomeTcInstr inp'))
-> TypeCheckedSeq op inp -> f (TypeCheckedSeq op inp')
mapMSeq (SomeTcInstr inp' -> Identity (SomeTcInstr inp')
forall a. a -> Identity a
Identity (SomeTcInstr inp' -> Identity (SomeTcInstr inp'))
-> (SomeTcInstr inp -> SomeTcInstr inp')
-> SomeTcInstr inp
-> Identity (SomeTcInstr inp')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeTcInstr inp -> SomeTcInstr inp'
f)
stackTypeComment :: HST st -> Instr st st
= ExtInstr st -> Instr st st
forall (inp :: [T]). ExtInstr inp -> Instr inp inp
Ext (ExtInstr st -> Instr st st)
-> (HST st -> ExtInstr st) -> HST st -> Instr st st
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommentType -> ExtInstr st
forall (s :: [T]). CommentType -> ExtInstr s
COMMENT_ITEM (CommentType -> ExtInstr st)
-> (HST st -> CommentType) -> HST st -> ExtInstr st
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe [T] -> CommentType
StackTypeComment (Maybe [T] -> CommentType)
-> (HST st -> Maybe [T]) -> HST st -> CommentType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [T] -> Maybe [T]
forall a. a -> Maybe a
Just ([T] -> Maybe [T]) -> (HST st -> [T]) -> HST st -> Maybe [T]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HST st -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs
noStackTypeComment :: Instr st st
= ExtInstr st -> Instr st st
forall (inp :: [T]). ExtInstr inp -> Instr inp inp
Ext (CommentType -> ExtInstr st
forall (s :: [T]). CommentType -> ExtInstr s
COMMENT_ITEM (Maybe [T] -> CommentType
StackTypeComment Maybe [T]
forall a. Maybe a
Nothing))
wrapWithLoc :: ErrorSrcPos -> TypeCheckedSeq op inp -> TypeCheckedSeq op inp
wrapWithLoc :: forall op (inp :: [T]).
ErrorSrcPos -> TypeCheckedSeq op inp -> TypeCheckedSeq op inp
wrapWithLoc ErrorSrcPos
loc = (SomeTcInstr inp -> SomeTcInstr inp)
-> TypeCheckedSeq op inp -> TypeCheckedSeq op inp
forall (inp :: [T]) (inp' :: [T]) op.
(SomeTcInstr inp -> SomeTcInstr inp')
-> TypeCheckedSeq op inp -> TypeCheckedSeq op inp'
mapSeq ((SomeTcInstr inp -> SomeTcInstr inp)
-> TypeCheckedSeq op inp -> TypeCheckedSeq op inp)
-> (SomeTcInstr inp -> SomeTcInstr inp)
-> TypeCheckedSeq op inp
-> TypeCheckedSeq op inp
forall a b. (a -> b) -> a -> b
$ \SomeTcInstr inp
someInstr -> case SomeTcInstr inp
someInstr of
(HST inp
_ :/ WithLoc{} ::: HST out
_) -> SomeTcInstr inp
someInstr
(HST inp
inp :/ Instr inp out
instr ::: HST out
out) -> HST inp
inp HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ ErrorSrcPos -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
ErrorSrcPos -> Instr inp out -> Instr inp out
WithLoc ErrorSrcPos
loc Instr inp out
instr Instr inp out -> HST out -> SomeTcInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: HST out
out
(HST inp
inp :/ AnyOutInstr forall (out :: [T]). Instr inp out
instr) -> HST inp
inp HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ ((forall (out :: [T]). Instr inp out) -> SomeTcInstrOut inp
forall (inp :: [T]).
(forall (out :: [T]). Instr inp out) -> SomeTcInstrOut inp
AnyOutInstr ((forall (out :: [T]). Instr inp out) -> SomeTcInstrOut inp)
-> (forall (out :: [T]). Instr inp out) -> SomeTcInstrOut inp
forall a b. (a -> b) -> a -> b
$ ErrorSrcPos -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
ErrorSrcPos -> Instr inp out -> Instr inp out
WithLoc ErrorSrcPos
loc Instr inp out
forall (out :: [T]). Instr inp out
instr)
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)
memImpl :: forall (c :: T) (memKey :: T) (rs :: [T]) (inp :: [T])
(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)
memImpl inputHST :: HST inp
inputHST@((SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
_ ::& HST xs
hstTail) VarAnn
varAnn =
case forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TcTypeError (a :~: b)
eqType @memKey @(MemOpKey c) of
Right memKey :~: MemOpKey c
Refl ->
SomeTcInstr inp -> m (SomeTcInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTcInstr inp -> m (SomeTcInstr inp))
-> SomeTcInstr inp -> m (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
inputHST HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/
AnnVar -> Instr (MemOpKey c : c : xs) ('TBool : xs)
forall (c :: T) (s :: [T]).
MemOp c =>
AnnVar -> Instr (MemOpKey c : c : s) ('TBool : s)
AnnMEM (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
varAnn) Instr inp ('TBool : xs) -> HST ('TBool : xs) -> SomeTcInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: ((SingT 'TBool
forall {k} (a :: k). SingI a => Sing a
sing, Dict (WellTyped 'TBool)
forall (a :: Constraint). a => Dict a
Dict) (SingT 'TBool, Dict (WellTyped 'TBool))
-> HST xs -> HST ('TBool : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
hstTail)
Left TcTypeError
m ->
InstrAbstract op
-> SomeHST
-> Maybe TypeContext
-> TcTypeError
-> m (SomeTcInstr inp)
forall (m :: * -> *) op a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) =>
InstrAbstract op
-> SomeHST -> Maybe TypeContext -> TcTypeError -> m a
typeCheckInstrErr' InstrAbstract op
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) TcTypeError
m
where
uInstr :: InstrAbstract op
uInstr = VarAnn -> InstrAbstract op
forall op. VarAnn -> InstrAbstract op
Un.MEM VarAnn
varAnn
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)
getImpl :: forall (c :: T) (getKey :: T) (rs :: [T]) (inp :: [T])
(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)
getImpl inputHST :: HST inp
inputHST@((SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
_ ::& HST xs
hstTail) SingT (GetOpVal c)
valueSing VarAnn
varAnn =
case forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TcTypeError (a :~: b)
eqType @getKey @(GetOpKey c) of
Right getKey :~: GetOpKey c
Refl ->
SomeTcInstr inp -> m (SomeTcInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTcInstr inp -> m (SomeTcInstr inp))
-> SomeTcInstr inp -> m (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
inputHST HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/
AnnVar -> Instr (GetOpKey c : c : rs) ('TOption (GetOpVal c) : rs)
forall (c :: T) (s :: [T]).
(GetOp c, SingI (GetOpVal c)) =>
AnnVar -> Instr (GetOpKey c : c : s) ('TOption (GetOpVal c) : s)
AnnGET (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
varAnn) Instr inp ('TOption (GetOpVal c) : xs)
-> HST ('TOption (GetOpVal c) : xs) -> SomeTcInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: ((Sing (GetOpVal c) -> SingT ('TOption (GetOpVal c))
forall (n :: T). Sing n -> SingT ('TOption n)
STOption Sing (GetOpVal c)
SingT (GetOpVal c)
valueSing, Dict (WellTyped ('TOption (GetOpVal c)))
forall (a :: Constraint). a => Dict a
Dict) (SingT ('TOption (GetOpVal c)),
Dict (WellTyped ('TOption (GetOpVal c))))
-> HST xs -> HST ('TOption (GetOpVal c) : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
hstTail)
Left TcTypeError
m ->
InstrAbstract op
-> SomeHST
-> Maybe TypeContext
-> TcTypeError
-> m (SomeTcInstr inp)
forall (m :: * -> *) op a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) =>
InstrAbstract op
-> SomeHST -> Maybe TypeContext -> TcTypeError -> m a
typeCheckInstrErr' InstrAbstract op
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) TcTypeError
m
where
uInstr :: InstrAbstract op
uInstr = VarAnn -> InstrAbstract op
forall op. VarAnn -> InstrAbstract op
Un.GET VarAnn
varAnn
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)
updImpl :: forall (c :: T) (updKey :: T) (updParams :: T) (rs :: [T])
(inp :: [T]) (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)
updImpl inputHST :: HST inp
inputHST@((SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
cTuple ::& HST xs
hstTail) VarAnn
varAnn =
case (forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TcTypeError (a :~: b)
eqType @updKey @(UpdOpKey c), forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TcTypeError (a :~: b)
eqType @updParams @(UpdOpParams c)) of
(Right updKey :~: UpdOpKey c
Refl, Right updParams :~: UpdOpParams c
Refl) ->
SomeTcInstr inp -> m (SomeTcInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTcInstr inp -> m (SomeTcInstr inp))
-> SomeTcInstr inp -> m (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
inputHST HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/
AnnVar -> Instr (UpdOpKey x : UpdOpParams x : x : xs) (x : xs)
forall (c :: T) (s :: [T]).
UpdOp c =>
AnnVar -> Instr (UpdOpKey c : UpdOpParams c : c : s) (c : s)
AnnUPDATE (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
varAnn) Instr inp (x : xs) -> HST (x : xs) -> SomeTcInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: ((SingT x, Dict (WellTyped x))
cTuple (SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
hstTail)
(Left TcTypeError
m, Either TcTypeError (updParams :~: UpdOpParams c)
_) ->
InstrAbstract op
-> SomeHST
-> Maybe TypeContext
-> TcTypeError
-> m (SomeTcInstr inp)
forall (m :: * -> *) op a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) =>
InstrAbstract op
-> SomeHST -> Maybe TypeContext -> TcTypeError -> m a
typeCheckInstrErr' InstrAbstract op
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) TcTypeError
m
(Either TcTypeError (updKey :~: UpdOpKey c)
_, Left TcTypeError
m) ->
InstrAbstract op
-> SomeHST
-> Maybe TypeContext
-> TcTypeError
-> m (SomeTcInstr inp)
forall (m :: * -> *) op a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) =>
InstrAbstract op
-> SomeHST -> Maybe TypeContext -> TcTypeError -> m a
typeCheckInstrErr' InstrAbstract op
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerValueType) TcTypeError
m
where
uInstr :: InstrAbstract op
uInstr = VarAnn -> InstrAbstract op
forall op. VarAnn -> InstrAbstract op
Un.UPDATE VarAnn
varAnn
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)
getUpdImpl :: forall (c :: T) (updKey :: T) (updParams :: T) (rs :: [T])
(inp :: [T]) (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)
getUpdImpl inputHST :: HST inp
inputHST@((SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
hst1 ::& (SingT x, Dict (WellTyped x))
cTuple ::& HST xs
hstTail) VarAnn
varAnn =
case (forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TcTypeError (a :~: b)
eqType @updKey @(UpdOpKey c), forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TcTypeError (a :~: b)
eqType @updParams @(UpdOpParams c)) of
(Right updKey :~: UpdOpKey c
Refl, Right updParams :~: 'TOption (GetOpVal c)
Refl) ->
SomeTcInstr inp -> m (SomeTcInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTcInstr inp -> m (SomeTcInstr inp))
-> SomeTcInstr inp -> m (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
inputHST HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/
AnnVar
-> Instr
(UpdOpKey c : UpdOpParams c : c : rs)
('TOption (GetOpVal c) : c : rs)
forall (c :: T) (s :: [T]).
(GetOp c, UpdOp c, SingI (GetOpVal c), UpdOpKey c ~ GetOpKey c) =>
AnnVar
-> Instr
(UpdOpKey c : UpdOpParams c : c : s)
('TOption (GetOpVal c) : c : s)
AnnGET_AND_UPDATE (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
varAnn) Instr inp (x : x : xs) -> HST (x : x : xs) -> SomeTcInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: ((SingT x, Dict (WellTyped x))
hst1 (SingT x, Dict (WellTyped x)) -> HST (x : xs) -> HST (x : x : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& (SingT x, Dict (WellTyped x))
cTuple (SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
hstTail)
(Left TcTypeError
m, Either TcTypeError (updParams :~: 'TOption (GetOpVal c))
_) ->
InstrAbstract op
-> SomeHST
-> Maybe TypeContext
-> TcTypeError
-> m (SomeTcInstr inp)
forall (m :: * -> *) op a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) =>
InstrAbstract op
-> SomeHST -> Maybe TypeContext -> TcTypeError -> m a
typeCheckInstrErr' InstrAbstract op
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) TcTypeError
m
(Either TcTypeError (updKey :~: UpdOpKey c)
_, Left TcTypeError
m) ->
InstrAbstract op
-> SomeHST
-> Maybe TypeContext
-> TcTypeError
-> m (SomeTcInstr inp)
forall (m :: * -> *) op a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) =>
InstrAbstract op
-> SomeHST -> Maybe TypeContext -> TcTypeError -> m a
typeCheckInstrErr' InstrAbstract op
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerValueType) TcTypeError
m
where
uInstr :: InstrAbstract op
uInstr = VarAnn -> InstrAbstract op
forall op. VarAnn -> InstrAbstract op
Un.GET_AND_UPDATE VarAnn
varAnn
sizeImpl
:: (SizeOp c, inp ~ (c ': rs), Monad m)
=> HST inp
-> VarAnn
-> m (SomeTcInstr inp)
sizeImpl :: forall (c :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(SizeOp c, inp ~ (c : rs), Monad m) =>
HST inp -> VarAnn -> m (SomeTcInstr inp)
sizeImpl i :: HST inp
i@((SingT x, Dict (WellTyped x))
_ ::& HST xs
rs) VarAnn
vn =
SomeTcInstr inp -> m (SomeTcInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTcInstr inp -> m (SomeTcInstr inp))
-> SomeTcInstr inp -> m (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ AnnVar -> Instr (c : xs) ('TNat : xs)
forall (c :: T) (s :: [T]).
SizeOp c =>
AnnVar -> Instr (c : s) ('TNat : s)
AnnSIZE (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
vn) Instr (c : xs) ('TNat : xs)
-> HST ('TNat : xs) -> SomeTcInstrOut (c : xs)
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: ((SingT 'TNat
forall {k} (a :: k). SingI a => Sing a
sing, Dict (WellTyped 'TNat)
forall (a :: Constraint). a => Dict a
Dict) (SingT 'TNat, Dict (WellTyped 'TNat)) -> HST xs -> HST ('TNat : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
rs)
sliceImpl
:: (SliceOp c, inp ~ ('TNat ': 'TNat ': c ': rs), Monad m)
=> HST inp
-> Un.VarAnn
-> m (SomeTcInstr inp)
sliceImpl :: forall (c :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(SliceOp c, inp ~ ('TNat : 'TNat : c : rs), Monad m) =>
HST inp -> VarAnn -> m (SomeTcInstr inp)
sliceImpl i :: HST inp
i@((SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
_ ::& (SingT x
cn, Dict (WellTyped x)
Dict) ::& HST xs
rs) VarAnn
vn = do
let rn :: SingT ('TOption c)
rn = Sing c -> SingT ('TOption c)
forall (n :: T). Sing n -> SingT ('TOption n)
STOption Sing c
SingT x
cn
SomeTcInstr inp -> m (SomeTcInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTcInstr inp -> m (SomeTcInstr inp))
-> SomeTcInstr inp -> m (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ AnnVar -> Instr ('TNat : 'TNat : c : xs) ('TOption c : xs)
forall (c :: T) (s :: [T]).
(SliceOp c, SingI c) =>
AnnVar -> Instr ('TNat : 'TNat : c : s) ('TOption c : s)
AnnSLICE (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
vn) Instr ('TNat : 'TNat : c : xs) ('TOption c : xs)
-> HST ('TOption c : xs) -> SomeTcInstrOut ('TNat : 'TNat : c : xs)
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: ((SingT ('TOption c)
rn, Dict (WellTyped ('TOption c))
forall (a :: Constraint). a => Dict a
Dict) (SingT ('TOption c), Dict (WellTyped ('TOption c)))
-> HST xs -> HST ('TOption c : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
rs)
concatImpl'
:: (ConcatOp c, WellTyped c, inp ~ ('TList c : rs), Monad m)
=> HST inp
-> Un.VarAnn
-> m (SomeTcInstr inp)
concatImpl' :: forall (c :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(ConcatOp c, WellTyped c, inp ~ ('TList c : rs), Monad m) =>
HST inp -> VarAnn -> m (SomeTcInstr inp)
concatImpl' i :: HST inp
i@((STList Sing n
n, Dict (WellTyped x)
Dict) ::& HST xs
rs) VarAnn
vn = do
SomeTcInstr inp -> m (SomeTcInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTcInstr inp -> m (SomeTcInstr inp))
-> SomeTcInstr inp -> m (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ AnnVar -> Instr ('TList c : xs) (c : xs)
forall (c :: T) (s :: [T]).
ConcatOp c =>
AnnVar -> Instr ('TList c : s) (c : s)
AnnCONCAT' (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
vn) Instr ('TList c : xs) (c : xs)
-> HST (c : xs) -> SomeTcInstrOut ('TList c : xs)
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: ((Sing n
SingT c
n, Dict (WellTyped c)
forall (a :: Constraint). a => Dict a
Dict) (SingT c, Dict (WellTyped c)) -> HST xs -> HST (c : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
rs)
concatImpl
:: ( ConcatOp c, inp ~ (c ': c ': rs)
, WellTyped c
, MonadReader TypeCheckInstrEnv m
)
=> HST inp
-> Un.VarAnn
-> m (SomeTcInstr inp)
concatImpl :: forall (c :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(ConcatOp c, inp ~ (c : c : rs), WellTyped c,
MonadReader TypeCheckInstrEnv m) =>
HST inp -> VarAnn -> m (SomeTcInstr inp)
concatImpl i :: HST inp
i@((SingT x
cn1, Dict (WellTyped x)
_) ::& (SingT x
_, Dict (WellTyped x)
_) ::& HST xs
rs) VarAnn
vn = do
SomeTcInstr inp -> m (SomeTcInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTcInstr inp -> m (SomeTcInstr inp))
-> SomeTcInstr inp -> m (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ AnnVar -> Instr (x : x : xs) (x : xs)
forall (c :: T) (s :: [T]).
ConcatOp c =>
AnnVar -> Instr (c : c : s) (c : s)
AnnCONCAT (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
vn) Instr (x : x : xs) (x : xs)
-> HST (x : xs) -> SomeTcInstrOut (x : x : xs)
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: ((SingT x
cn1, Dict (WellTyped x)
forall (a :: Constraint). a => Dict a
Dict) (SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
rs)
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
-> Un.InstrAbstract op
-> t (SomeTcInstr inp)
arithImpl :: forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl AnnVar -> Instr inp (ArithRes aop n m : s)
mkInstr i :: HST inp
i@((SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
_ ::& HST xs
rs) VarAnn
vn InstrAbstract op
_ =
SomeTcInstr inp -> t (SomeTcInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTcInstr inp -> t (SomeTcInstr inp))
-> SomeTcInstr inp -> t (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ AnnVar -> Instr inp (ArithRes aop n m : s)
mkInstr (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
vn) Instr inp (ArithRes aop n m : xs)
-> HST (ArithRes aop n m : xs) -> SomeTcInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: ((SingT (ArithRes aop n m)
forall {k} (a :: k). SingI a => Sing a
sing, Dict (WellTyped (ArithRes aop n m))
forall (a :: Constraint). a => Dict a
Dict) (SingT (ArithRes aop n m), Dict (WellTyped (ArithRes aop n m)))
-> HST xs -> HST (ArithRes aop n m : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
rs)
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
-> Un.InstrAbstract op
-> m (SomeTcInstr inp)
addImpl :: forall (a :: T) (b :: T) (inp :: [T]) (rs :: [T]) (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)
addImpl Sing a
t1 Sing b
t2 = case (Sing a
SingT a
t1, Sing b
SingT b
t2) of
(SingT a
STInt, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Add AnnVar
-> Instr ('TInt : 'TInt : rs) (ArithRes Add 'TInt 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STInt, SingT b
STNat) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Add AnnVar
-> Instr ('TInt : 'TNat : rs) (ArithRes Add 'TInt 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STNat, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Add AnnVar
-> Instr ('TNat : 'TInt : rs) (ArithRes Add 'TNat 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STNat, SingT b
STNat) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Add AnnVar
-> Instr ('TNat : 'TNat : rs) (ArithRes Add 'TNat 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STInt, SingT b
STTimestamp) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Add AnnVar
-> Instr
('TInt : 'TTimestamp : rs) (ArithRes Add 'TInt 'TTimestamp : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STTimestamp, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Add AnnVar
-> Instr
('TTimestamp : 'TInt : rs) (ArithRes Add 'TTimestamp 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STMutez, SingT b
STMutez) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Add AnnVar
-> Instr
('TMutez : 'TMutez : rs) (ArithRes Add 'TMutez 'TMutez : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STBls12381Fr, SingT b
STBls12381Fr) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Add AnnVar
-> Instr
('TBls12381Fr : 'TBls12381Fr : rs)
(ArithRes Add 'TBls12381Fr 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STBls12381G1, SingT b
STBls12381G1) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Add AnnVar
-> Instr
('TBls12381G1 : 'TBls12381G1 : rs)
(ArithRes Add 'TBls12381G1 'TBls12381G1 : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STBls12381G2, SingT b
STBls12381G2) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Add AnnVar
-> Instr
('TBls12381G2 : 'TBls12381G2 : rs)
(ArithRes Add 'TBls12381G2 'TBls12381G2 : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a, SingT b)
_ -> \HST inp
i VarAnn
_ InstrAbstract op
uInstr -> InstrAbstract op
-> SomeHST
-> Maybe TypeContext
-> TcTypeError
-> m (SomeTcInstr inp)
forall (m :: * -> *) op a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) =>
InstrAbstract op
-> SomeHST -> Maybe TypeContext -> TcTypeError -> m a
typeCheckInstrErr' InstrAbstract op
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TcTypeError -> m (SomeTcInstr inp))
-> TcTypeError -> m (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$
T -> T -> TcTypeError
NotNumericTypes (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @a) (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @b)
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
-> Un.InstrAbstract op
-> m (SomeTcInstr inp)
edivImpl :: forall (a :: T) (b :: T) (inp :: [T]) (rs :: [T]) (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)
edivImpl Sing a
t1 Sing b
t2 = case (Sing a
SingT a
t1, Sing b
SingT b
t2) of
(SingT a
STInt, SingT b
STInt) -> HST inp -> VarAnn -> InstrAbstract op -> m (SomeTcInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *) op.
(ArithOp EDiv n m,
ArithRes EDiv n m
~ 'TOption ('TPair (EDivOpRes n m) (EModOpRes n m)),
WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
inp ~ (n : m : s), MonadReader TypeCheckInstrEnv t) =>
HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
edivImplDo
(SingT a
STInt, SingT b
STNat) -> HST inp -> VarAnn -> InstrAbstract op -> m (SomeTcInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *) op.
(ArithOp EDiv n m,
ArithRes EDiv n m
~ 'TOption ('TPair (EDivOpRes n m) (EModOpRes n m)),
WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
inp ~ (n : m : s), MonadReader TypeCheckInstrEnv t) =>
HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
edivImplDo
(SingT a
STNat, SingT b
STInt) -> HST inp -> VarAnn -> InstrAbstract op -> m (SomeTcInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *) op.
(ArithOp EDiv n m,
ArithRes EDiv n m
~ 'TOption ('TPair (EDivOpRes n m) (EModOpRes n m)),
WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
inp ~ (n : m : s), MonadReader TypeCheckInstrEnv t) =>
HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
edivImplDo
(SingT a
STNat, SingT b
STNat) -> HST inp -> VarAnn -> InstrAbstract op -> m (SomeTcInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *) op.
(ArithOp EDiv n m,
ArithRes EDiv n m
~ 'TOption ('TPair (EDivOpRes n m) (EModOpRes n m)),
WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
inp ~ (n : m : s), MonadReader TypeCheckInstrEnv t) =>
HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
edivImplDo
(SingT a
STMutez, SingT b
STMutez) -> HST inp -> VarAnn -> InstrAbstract op -> m (SomeTcInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *) op.
(ArithOp EDiv n m,
ArithRes EDiv n m
~ 'TOption ('TPair (EDivOpRes n m) (EModOpRes n m)),
WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
inp ~ (n : m : s), MonadReader TypeCheckInstrEnv t) =>
HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
edivImplDo
(SingT a
STMutez, SingT b
STNat) -> HST inp -> VarAnn -> InstrAbstract op -> m (SomeTcInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *) op.
(ArithOp EDiv n m,
ArithRes EDiv n m
~ 'TOption ('TPair (EDivOpRes n m) (EModOpRes n m)),
WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
inp ~ (n : m : s), MonadReader TypeCheckInstrEnv t) =>
HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
edivImplDo
(SingT a, SingT b)
_ -> \HST inp
i VarAnn
_ InstrAbstract op
uInstr -> InstrAbstract op
-> SomeHST
-> Maybe TypeContext
-> TcTypeError
-> m (SomeTcInstr inp)
forall (m :: * -> *) op a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) =>
InstrAbstract op
-> SomeHST -> Maybe TypeContext -> TcTypeError -> m a
typeCheckInstrErr' InstrAbstract op
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TcTypeError -> m (SomeTcInstr inp))
-> TcTypeError -> m (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$
T -> T -> TcTypeError
NotNumericTypes (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @a) (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @b)
edivImplDo
:: ( ArithOp EDiv n m
, ArithRes EDiv n m ~ 'TOption ('TPair (EDivOpRes n m) (EModOpRes n m))
, WellTyped (EModOpRes n m)
, WellTyped (EDivOpRes n m)
, inp ~ (n ': m ': s)
, MonadReader TypeCheckInstrEnv t
)
=> HST inp
-> VarAnn
-> Un.InstrAbstract op
-> t (SomeTcInstr inp)
edivImplDo :: forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *) op.
(ArithOp EDiv n m,
ArithRes EDiv n m
~ 'TOption ('TPair (EDivOpRes n m) (EModOpRes n m)),
WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
inp ~ (n : m : s), MonadReader TypeCheckInstrEnv t) =>
HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
edivImplDo i :: HST inp
i@((SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
_ ::& HST xs
rs) VarAnn
vn InstrAbstract op
_ =
SomeTcInstr inp -> t (SomeTcInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTcInstr inp -> t (SomeTcInstr inp))
-> SomeTcInstr inp -> t (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ AnnVar -> Instr (n : m : s) (ArithRes EDiv n m : s)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp EDiv n m =>
AnnVar -> Instr (n : m : s) (ArithRes EDiv n m : s)
AnnEDIV (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
vn) Instr
(n : m : s)
('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : xs)
-> HST ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : xs)
-> SomeTcInstrOut (n : m : s)
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: ((SingT ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
forall {k} (a :: k). SingI a => Sing a
sing, Dict
(WellTyped ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m))))
forall (a :: Constraint). a => Dict a
Dict) (SingT ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m))),
Dict
(WellTyped ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))))
-> HST xs
-> HST ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
rs)
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
-> Un.InstrAbstract op
-> m (SomeTcInstr inp)
subImpl :: forall (a :: T) (b :: T) (inp :: [T]) (rs :: [T]) (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 Sing a
t1 Sing b
t2 = case (Sing a
SingT a
t1, Sing b
SingT b
t2) of
(SingT a
STInt, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Sub AnnVar
-> Instr ('TInt : 'TInt : rs) (ArithRes Sub 'TInt 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Sub n m =>
AnnVar -> Instr (n : m : s) (ArithRes Sub n m : s)
AnnSUB
(SingT a
STInt, SingT b
STNat) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Sub AnnVar
-> Instr ('TInt : 'TNat : rs) (ArithRes Sub 'TInt 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Sub n m =>
AnnVar -> Instr (n : m : s) (ArithRes Sub n m : s)
AnnSUB
(SingT a
STNat, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Sub AnnVar
-> Instr ('TNat : 'TInt : rs) (ArithRes Sub 'TNat 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Sub n m =>
AnnVar -> Instr (n : m : s) (ArithRes Sub n m : s)
AnnSUB
(SingT a
STNat, SingT b
STNat) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Sub AnnVar
-> Instr ('TNat : 'TNat : rs) (ArithRes Sub 'TNat 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Sub n m =>
AnnVar -> Instr (n : m : s) (ArithRes Sub n m : s)
AnnSUB
(SingT a
STTimestamp, SingT b
STTimestamp) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Sub AnnVar
-> Instr
('TTimestamp : 'TTimestamp : rs)
(ArithRes Sub 'TTimestamp 'TTimestamp : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Sub n m =>
AnnVar -> Instr (n : m : s) (ArithRes Sub n m : s)
AnnSUB
(SingT a
STMutez, SingT b
STMutez) -> \HST inp
i VarAnn
_ InstrAbstract op
uInstr -> InstrAbstract op
-> SomeHST
-> Maybe TypeContext
-> TcTypeError
-> m (SomeTcInstr inp)
forall (m :: * -> *) op a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) =>
InstrAbstract op
-> SomeHST -> Maybe TypeContext -> TcTypeError -> m a
typeCheckInstrErr' InstrAbstract op
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TcTypeError -> m (SomeTcInstr inp))
-> TcTypeError -> m (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$
InstrAbstract () -> Text -> TcTypeError
InvalidInstruction (InstrAbstract op
uInstr InstrAbstract op -> () -> InstrAbstract ()
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ()) Text
"Use of SUB on `mutez` operands is deprecated; use SUB_MUTEZ"
(SingT a
STTimestamp, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Sub AnnVar
-> Instr
('TTimestamp : 'TInt : rs) (ArithRes Sub 'TTimestamp 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Sub n m =>
AnnVar -> Instr (n : m : s) (ArithRes Sub n m : s)
AnnSUB
(SingT a, SingT b)
_ -> \HST inp
i VarAnn
_ InstrAbstract op
uInstr -> InstrAbstract op
-> SomeHST
-> Maybe TypeContext
-> TcTypeError
-> m (SomeTcInstr inp)
forall (m :: * -> *) op a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) =>
InstrAbstract op
-> SomeHST -> Maybe TypeContext -> TcTypeError -> m a
typeCheckInstrErr' InstrAbstract op
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TcTypeError -> m (SomeTcInstr inp))
-> TcTypeError -> m (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$
T -> T -> TcTypeError
NotNumericTypes (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @a) (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @b)
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
-> Un.InstrAbstract op
-> m (SomeTcInstr inp)
mulImpl :: forall (a :: T) (b :: T) (inp :: [T]) (rs :: [T]) (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 Sing a
t1 Sing b
t2 = case (Sing a
SingT a
t1, Sing b
SingT b
t2) of
(SingT a
STInt, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Mul AnnVar
-> Instr ('TInt : 'TInt : rs) (ArithRes Mul 'TInt 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STInt, SingT b
STNat) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Mul AnnVar
-> Instr ('TInt : 'TNat : rs) (ArithRes Mul 'TInt 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STNat, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Mul AnnVar
-> Instr ('TNat : 'TInt : rs) (ArithRes Mul 'TNat 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STNat, SingT b
STNat) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Mul AnnVar
-> Instr ('TNat : 'TNat : rs) (ArithRes Mul 'TNat 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STNat, SingT b
STMutez) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Mul AnnVar
-> Instr ('TNat : 'TMutez : rs) (ArithRes Mul 'TNat 'TMutez : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STMutez, SingT b
STNat) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Mul AnnVar
-> Instr ('TMutez : 'TNat : rs) (ArithRes Mul 'TMutez 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STInt, SingT b
STBls12381Fr) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Mul AnnVar
-> Instr
('TInt : 'TBls12381Fr : rs) (ArithRes Mul 'TInt 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STNat, SingT b
STBls12381Fr) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Mul AnnVar
-> Instr
('TNat : 'TBls12381Fr : rs) (ArithRes Mul 'TNat 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STBls12381Fr, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Mul AnnVar
-> Instr
('TBls12381Fr : 'TInt : rs) (ArithRes Mul 'TBls12381Fr 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STBls12381Fr, SingT b
STNat) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Mul AnnVar
-> Instr
('TBls12381Fr : 'TNat : rs) (ArithRes Mul 'TBls12381Fr 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STBls12381Fr, SingT b
STBls12381Fr) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Mul AnnVar
-> Instr
('TBls12381Fr : 'TBls12381Fr : rs)
(ArithRes Mul 'TBls12381Fr 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STBls12381G1, SingT b
STBls12381Fr) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Mul AnnVar
-> Instr
('TBls12381G1 : 'TBls12381Fr : rs)
(ArithRes Mul 'TBls12381G1 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STBls12381G2, SingT b
STBls12381Fr) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *) op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *)
op.
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> InstrAbstract op -> t (SomeTcInstr inp)
arithImpl @Mul AnnVar
-> Instr
('TBls12381G2 : 'TBls12381Fr : rs)
(ArithRes Mul 'TBls12381G2 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a, SingT b)
_ -> \HST inp
i VarAnn
_ InstrAbstract op
uInstr -> InstrAbstract op
-> SomeHST
-> Maybe TypeContext
-> TcTypeError
-> m (SomeTcInstr inp)
forall (m :: * -> *) op a.
(MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) =>
InstrAbstract op
-> SomeHST -> Maybe TypeContext -> TcTypeError -> m a
typeCheckInstrErr' InstrAbstract op
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TcTypeError -> m (SomeTcInstr inp))
-> TcTypeError -> m (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$
T -> T -> TcTypeError
NotNumericTypes (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @a) (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @b)
unaryArithImpl
:: ( WellTyped (UnaryArithRes aop n)
, inp ~ (n ': s)
, Monad t
)
=> Instr inp (UnaryArithRes aop n ': s)
-> HST inp
-> t (SomeTcInstr inp)
unaryArithImpl :: forall {k} (aop :: k) (n :: T) (inp :: [T]) (s :: [T])
(t :: * -> *).
(WellTyped (UnaryArithRes aop n), inp ~ (n : s), Monad t) =>
Instr inp (UnaryArithRes aop n : s)
-> HST inp -> t (SomeTcInstr inp)
unaryArithImpl Instr inp (UnaryArithRes aop n : s)
mkInstr i :: HST inp
i@((SingT x, Dict (WellTyped x))
_ ::& HST xs
rs) = do
SomeTcInstr inp -> t (SomeTcInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTcInstr inp -> t (SomeTcInstr inp))
-> SomeTcInstr inp -> t (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ Instr inp (UnaryArithRes aop n : s)
Instr inp (UnaryArithRes aop n : xs)
mkInstr Instr inp (UnaryArithRes aop n : xs)
-> HST (UnaryArithRes aop n : xs) -> SomeTcInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: ((SingT (UnaryArithRes aop n)
forall {k} (a :: k). SingI a => Sing a
sing, Dict (WellTyped (UnaryArithRes aop n))
forall (a :: Constraint). a => Dict a
Dict) (SingT (UnaryArithRes aop n),
Dict (WellTyped (UnaryArithRes aop n)))
-> HST xs -> HST (UnaryArithRes aop n : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
rs)
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)
unaryArithImplAnnotated :: forall {k} (aop :: k) (n :: T) (inp :: [T]) (s :: [T])
(t :: * -> *).
(WellTyped (UnaryArithRes aop n), inp ~ (n : s), Monad t,
n ~ UnaryArithRes aop n) =>
Instr inp (UnaryArithRes aop n : s)
-> HST inp -> t (SomeTcInstr inp)
unaryArithImplAnnotated Instr inp (UnaryArithRes aop n : s)
mkInstr i :: HST inp
i@((SingT x
n, Dict (WellTyped x)
_) ::& HST xs
rs) = do
SomeTcInstr inp -> t (SomeTcInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTcInstr inp -> t (SomeTcInstr inp))
-> SomeTcInstr inp -> t (SomeTcInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ Instr inp (x : xs)
Instr inp (UnaryArithRes aop n : s)
mkInstr Instr inp (x : xs) -> HST (x : xs) -> SomeTcInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: ((SingT x
n, Dict (WellTyped x)
forall (a :: Constraint). a => Dict a
Dict) (SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
rs)
checkContractDeprecations :: forall cp st op. Contract cp st -> Either (TcError' op) ()
checkContractDeprecations :: forall (cp :: T) (st :: T) op.
Contract cp st -> Either (TcError' op) ()
checkContractDeprecations Contract{} =
SingT cp -> Either (TcError' op) ()
forall (t :: T) op. SingT t -> Either (TcError' op) ()
checkSingDeprecations (forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @cp) Either (TcError' op) ()
-> Either (TcError' op) () -> Either (TcError' op) ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SingT st -> Either (TcError' op) ()
forall (t :: T) op. SingT t -> Either (TcError' op) ()
checkSingDeprecations (forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @st)
checkSingDeprecations :: SingT t -> Either (TcError' op) ()
checkSingDeprecations :: forall (t :: T) op. SingT t -> Either (TcError' op) ()
checkSingDeprecations SingT t
s
| T
ty : [T]
_ <- (T -> Bool) -> GenericQ [T]
forall r. Typeable r => (r -> Bool) -> GenericQ [r]
listify T -> Bool
isTimeLockTy (Sing t -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
SingT t
s) = T -> Either (TcError' op) ()
forall op' a. T -> Either (TcError' op') a
timelockDeprecated T
ty
| Bool
otherwise = Either (TcError' op) ()
forall (f :: * -> *). Applicative f => f ()
pass
where
isTimeLockTy :: T -> Bool
isTimeLockTy :: T -> Bool
isTimeLockTy T
TChest = Bool
True
isTimeLockTy T
TChestKey = Bool
True
isTimeLockTy T
_ = Bool
False
timelockDeprecated :: T -> Either (TcError' op') a
timelockDeprecated :: forall op' a. T -> Either (TcError' op') a
timelockDeprecated = TcError' op' -> Either (TcError' op') a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TcError' op' -> Either (TcError' op') a)
-> (T -> TcError' op') -> T -> Either (TcError' op') a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> T -> TcError' op'
forall op. Text -> T -> TcError' op
TcDeprecatedType
Text
"Timelock mechanism is affected by a vulnerability."