-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

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

import Prelude hiding (EQ, GT, LT)

import Control.Monad.Except (MonadError, catchError, 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, 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)

-- | Extract singleton for each single type of the given stack.
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

-- | Check whether the given stack types are equal.
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

-- | Check whether the given stack has size 1 and its only element matches the
-- given type. This function is a specialized version of `eqHST`.
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

--------------------------------------------
-- Typechecker auxiliary
--------------------------------------------

-- | Check whether elements go in strictly ascending order and
-- return the original list (to keep only one pass on the original list).
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

-- | Flipped version of 'catchError'.
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

-- | Function @eqType@ is a simple wrapper around @Data.Singletons.decideEquality@ suited
-- for use within @Either TcTypeError a@ applicative.
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

-- | Like 'typeCheckImpl' but doesn't add a stack type comment after the
-- sequence.
typeCheckImplNoLastTypeComment
  :: IsInstrOp op
  => TcInstrBase op
  -> TcInstr op [op]
typeCheckImplNoLastTypeComment :: forall op. IsInstrOp op => TcInstrBase op -> TcInstr op [op]
typeCheckImplNoLastTypeComment 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

-- | Like 'typeCheckImpl' but without the first and the last stack type
-- comments. Useful to reduce duplication of stack type comments.
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 -> ()
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op')
        (ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity)))
     ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      (Sing x
_ :: Sing t, Dict (WellTyped x)
_) ::& HST xs
_
        | T
ty : [T]
_ <- (T -> Bool) -> GenericQ [T]
forall r. Typeable r => (r -> Bool) -> GenericQ [r]
listify T -> Bool
isTimeLockTy (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @t) -> T -> TypeCheckInstr op' ()
forall op' a. T -> TypeCheckInstr op' a
timelockDeprecated T
ty
      (SingT x, Dict (WellTyped x))
_ ::& HST xs
xs -> HST xs -> TypeCheckInstr op' ()
forall (a :: [T]) op'. HST a -> TypeCheckInstr op' ()
doCheckBadTypes HST xs
xs
    isTimeLockTy :: T -> Bool
    isTimeLockTy :: T -> Bool
isTimeLockTy T
TChest = Bool
True
    isTimeLockTy T
TChestKey = Bool
True
    isTimeLockTy T
_ = Bool
False
    timelockDeprecated :: T -> TypeCheckInstr op' a
    timelockDeprecated :: forall op' a. T -> TypeCheckInstr op' a
timelockDeprecated = TcError' op'
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op')
        (ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity)))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TcError' op'
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op')
         (ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity)))
      a)
-> (T -> TcError' op')
-> T
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op')
        (ReaderT TypeCheckOptions (ExceptT (TcError' op') Identity)))
     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."


prependStackTypeComment
  :: SomeTcInstr inp -> TypeCheckInstrNoExcept op (SomeTcInstr inp)
prependStackTypeComment :: forall (inp :: [T]) op.
SomeTcInstr inp -> TypeCheckInstrNoExcept op (SomeTcInstr inp)
prependStackTypeComment 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
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 (FrameInstr Proxy s
_ Instr a b
i) = Instr a b -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr a b
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
stackTypeComment :: forall (st :: [T]). HST st -> Instr st st
stackTypeComment = 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
noStackTypeComment :: forall (inp :: [T]). Instr inp inp
noStackTypeComment = 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)

--------------------------------------------
-- Some generic instruction implementation
--------------------------------------------

-- | Generic implementation for MEMeration
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)

-- | Helper function to construct instructions for binary arithmetic
-- operations.
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)

-- | Helper function to construct instructions for unary arithmetic
-- operations.
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)

-- | Helper function to construct instructions for unary arithmetic
-- operations that should preserve annotations.
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)