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

    , 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.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 m)
  => Un.ExpandedInstr -> SomeHST -> Maybe TypeContext
  -> Either TCTypeError a -> m a
onTypeCheckInstrErr :: forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr
-> SomeHST -> Maybe TypeContext -> Either TCTypeError a -> m a
onTypeCheckInstrErr ExpandedInstr
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 (ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
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) m a.
      (MonadReader TypeCheckInstrEnv m, MonadError TCError m, SingI t)
  => Un.ExpandedInstr -> SomeHST -> Maybe TypeContext
  -> Either BadTypeForScope a -> m a
onScopeCheckInstrErr :: forall (t :: T) (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m, SingI t) =>
ExpandedInstr
-> SomeHST -> Maybe TypeContext -> Either BadTypeForScope a -> m a
onScopeCheckInstrErr ExpandedInstr
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 -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> m a) -> TCError -> m a
forall a b. (a -> b) -> a -> b
$ ExpandedInstr
-> SomeHST
-> ErrorSrcPos
-> Maybe TypeContext
-> Maybe TCTypeError
-> TCError
TCFailedOnInstr ExpandedInstr
instr SomeHST
hst ErrorSrcPos
pos Maybe TypeContext
mContext (Maybe TCTypeError -> TCError) -> Maybe TCTypeError -> TCError
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 m)
  => Un.ExpandedInstr -> SomeHST -> Maybe TypeContext
  -> m a
typeCheckInstrErr :: forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> m a
typeCheckInstrErr ExpandedInstr
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 -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> m a) -> TCError -> m a
forall a b. (a -> b) -> a -> b
$ ExpandedInstr
-> SomeHST
-> ErrorSrcPos
-> Maybe TypeContext
-> Maybe TCTypeError
-> TCError
TCFailedOnInstr ExpandedInstr
instr SomeHST
hst ErrorSrcPos
pos Maybe TypeContext
mContext Maybe TCTypeError
forall a. Maybe a
Nothing

typeCheckInstrErr'
  :: (MonadReader TypeCheckInstrEnv m, MonadError TCError m)
  => Un.ExpandedInstr -> SomeHST -> Maybe TypeContext
  -> TCTypeError -> m a
typeCheckInstrErr' :: forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
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 -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> m a) -> TCError -> m a
forall a b. (a -> b) -> a -> b
$ ExpandedInstr
-> SomeHST
-> ErrorSrcPos
-> Maybe TypeContext
-> Maybe TCTypeError
-> TCError
TCFailedOnInstr ExpandedInstr
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. (SingI ts, MonadReader TypeCheckInstrEnv m, MonadError TCError m)
  => Sing a
  -> Un.ExpandedInstr
  -> HST ts
  -> (Comparable a => v)
  -> m v
withCompareableCheck :: forall (a :: T) (m :: * -> *) v (ts :: [T]).
(SingI ts, MonadReader TypeCheckInstrEnv m,
 MonadError TCError m) =>
Sing a -> ExpandedInstr -> HST ts -> (Comparable a => v) -> m v
withCompareableCheck Sing a
sng ExpandedInstr
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 -> ExpandedInstr -> SomeHST -> Maybe TypeContext -> m v
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> m a
typeCheckInstrErr ExpandedInstr
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

typeCheckOpImpl
  :: forall inp. SingI inp
  => TcInstrHandler
  -> Un.ExpandedOp
  -> HST inp
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl :: forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op' HST inp
hst = case ExpandedOp
op' of
  Un.WithSrcEx ErrorSrcPos
_ op :: ExpandedOp
op@Un.WithSrcEx{} -> TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op HST inp
hst
  Un.WithSrcEx ErrorSrcPos
loc (Un.PrimEx ExpandedInstr
op)  -> ErrorSrcPos
-> ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrimWithLoc ErrorSrcPos
loc ExpandedInstr
op
  Un.WithSrcEx ErrorSrcPos
loc (Un.SeqEx [ExpandedOp]
sq)   -> ErrorSrcPos
-> [ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeqWithLoc ErrorSrcPos
loc [ExpandedOp]
sq
  Un.PrimEx ExpandedInstr
op                     -> ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrim ExpandedInstr
op
  Un.SeqEx [ExpandedOp]
sq                      -> [ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeq [ExpandedOp]
sq
  where
    -- If we know source location from the untyped instruction, keep it in the typed one.
    typeCheckPrimWithLoc :: ErrorSrcPos -> Un.ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
    typeCheckPrimWithLoc :: ErrorSrcPos
-> ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrimWithLoc ErrorSrcPos
loc ExpandedInstr
op = (TypeCheckInstrEnv -> TypeCheckInstrEnv)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (ASetter TypeCheckInstrEnv TypeCheckInstrEnv ErrorSrcPos ErrorSrcPos
-> ErrorSrcPos -> TypeCheckInstrEnv -> TypeCheckInstrEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TypeCheckInstrEnv TypeCheckInstrEnv ErrorSrcPos ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos ErrorSrcPos
loc)
      (ErrorSrcPos -> TypeCheckedSeq inp -> TypeCheckedSeq inp
forall (inp :: [T]).
ErrorSrcPos -> TypeCheckedSeq inp -> TypeCheckedSeq inp
wrapWithLoc ErrorSrcPos
loc (TypeCheckedSeq inp -> TypeCheckedSeq inp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrim ExpandedInstr
op)

    typeCheckPrim :: Un.ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
    typeCheckPrim :: ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrim ExpandedInstr
op = ExpandedInstr
-> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
TcInstrHandler
tcInstr ExpandedInstr
op HST inp
hst

    typeCheckSeqWithLoc :: ErrorSrcPos -> [Un.ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
    typeCheckSeqWithLoc :: ErrorSrcPos
-> [ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeqWithLoc ErrorSrcPos
loc = (TypeCheckedSeq inp -> TypeCheckedSeq inp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ErrorSrcPos -> TypeCheckedSeq inp -> TypeCheckedSeq inp
forall (inp :: [T]).
ErrorSrcPos -> TypeCheckedSeq inp -> TypeCheckedSeq inp
wrapWithLoc ErrorSrcPos
loc) (ReaderT
   TypeCheckInstrEnv
   (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
   (TypeCheckedSeq inp)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
      (TypeCheckedSeq inp))
-> ([ExpandedOp]
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
         (TypeCheckedSeq inp))
-> [ExpandedOp]
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeCheckInstrEnv -> TypeCheckInstrEnv)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (ASetter TypeCheckInstrEnv TypeCheckInstrEnv ErrorSrcPos ErrorSrcPos
-> ErrorSrcPos -> TypeCheckInstrEnv -> TypeCheckInstrEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TypeCheckInstrEnv TypeCheckInstrEnv ErrorSrcPos ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos ErrorSrcPos
loc) (ReaderT
   TypeCheckInstrEnv
   (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
   (TypeCheckedSeq inp)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
      (TypeCheckedSeq inp))
-> ([ExpandedOp]
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
         (TypeCheckedSeq inp))
-> [ExpandedOp]
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ExpandedOp]
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
[ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeq

    typeCheckSeq :: [Un.ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
    typeCheckSeq :: [ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeq [ExpandedOp]
sq = TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl TcInstrHandler
tcInstr [ExpandedOp]
sq HST inp
hst
                  ReaderT
  TypeCheckInstrEnv
  (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
  (TypeCheckedSeq inp)
-> (TypeCheckedSeq inp -> TypeCheckedSeq inp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (SomeInstr inp -> SomeInstr inp)
-> TypeCheckedSeq inp -> TypeCheckedSeq inp
forall (inp :: [T]) (inp' :: [T]).
(SomeInstr inp -> SomeInstr inp')
-> TypeCheckedSeq inp -> TypeCheckedSeq inp'
mapSeq ((forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeInstr inp -> SomeInstr inp
forall (inp :: [T]).
(forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeInstr inp -> SomeInstr inp
mapSomeInstr forall (out :: [T]). Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
Nested)

-- | Like 'typeCheckImpl' but doesn't add a stack type comment after the
-- sequence.
typeCheckImplNoLastTypeComment
  :: forall inp . SingI inp
  => TcInstrHandler
  -> [Un.ExpandedOp]
  -> HST inp
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment :: forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment TcInstrHandler
_ [] HST inp
inputStack
  = TypeCheckedSeq inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> TypeCheckedSeq inp
forall (inp :: [T]). SomeInstr inp -> TypeCheckedSeq inp
WellTypedSeq (HST inp
inputStack HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop Instr inp inp -> HST inp -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST inp
inputStack))
typeCheckImplNoLastTypeComment TcInstrHandler
tcInstr [ExpandedOp
op] HST inp
inputStack = do
  TcInstrHandler
-> ExpandedOp
-> HST inp
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv, TypeCheckOptions]
     Identity
     (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op HST inp
inputStack
      ReaderT
  TypeCheckInstrEnv
  (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
  (TypeCheckedSeq inp)
-> (TypeCheckedSeq inp
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
         (TypeCheckedSeq inp))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (SomeInstr inp
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
      (SomeInstr inp))
-> TypeCheckedSeq inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall (f :: * -> *) (inp :: [T]) (inp' :: [T]).
Applicative f =>
(SomeInstr inp -> f (SomeInstr inp'))
-> TypeCheckedSeq inp -> f (TypeCheckedSeq inp')
mapMSeq SomeInstr inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (SomeInstr inp)
forall (inp :: [T]).
SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp)
prependStackTypeComment
typeCheckImplNoLastTypeComment TcInstrHandler
tcInstr (ExpandedOp
op : [ExpandedOp]
ops) HST inp
inputStack = do
  TypeCheckedSeq inp
done <- TcInstrHandler
-> ExpandedOp
-> HST inp
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv, TypeCheckOptions]
     Identity
     (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op HST inp
inputStack
      ReaderT
  TypeCheckInstrEnv
  (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
  (TypeCheckedSeq inp)
-> (TypeCheckedSeq inp
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
         (TypeCheckedSeq inp))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (SomeInstr inp
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
      (SomeInstr inp))
-> TypeCheckedSeq inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall (f :: * -> *) (inp :: [T]) (inp' :: [T]).
Applicative f =>
(SomeInstr inp -> f (SomeInstr inp'))
-> TypeCheckedSeq inp -> f (TypeCheckedSeq inp')
mapMSeq SomeInstr inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (SomeInstr inp)
forall (inp :: [T]).
SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp)
prependStackTypeComment
  TcInstrHandler
-> TypeCheckedSeq inp
-> [ExpandedOp]
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv, TypeCheckOptions]
     Identity
     (TypeCheckedSeq inp)
forall (inp :: [T]).
TcInstrHandler
-> TypeCheckedSeq inp
-> [ExpandedOp]
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
continueTypeChecking TcInstrHandler
tcInstr TypeCheckedSeq inp
done [ExpandedOp]
ops

continueTypeChecking
  :: forall inp. ()
  => TcInstrHandler
  -> TypeCheckedSeq inp
  -> [Un.ExpandedOp]
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
continueTypeChecking :: forall (inp :: [T]).
TcInstrHandler
-> TypeCheckedSeq inp
-> [ExpandedOp]
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
continueTypeChecking TcInstrHandler
tcInstr TypeCheckedSeq inp
done [ExpandedOp]
rest = case TypeCheckedSeq inp
done of
  WellTypedSeq SomeInstr inp
instr -> SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
handleFirst SomeInstr inp
instr
  MixedSeq SomeInstr inp
i TCError
e [IllTypedInstr]
left -> TypeCheckedSeq inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
forall (inp :: [T]).
SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
MixedSeq SomeInstr inp
i TCError
e ([IllTypedInstr]
left [IllTypedInstr] -> [IllTypedInstr] -> [IllTypedInstr]
forall a. Semigroup a => a -> a -> a
<> (ExpandedOp -> IllTypedInstr) -> [ExpandedOp] -> [IllTypedInstr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map ExpandedOp -> IllTypedInstr
NonTypedInstr [ExpandedOp]
rest))
  IllTypedSeq TCError
e [IllTypedInstr]
left -> TypeCheckedSeq inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
forall (inp :: [T]).
TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
IllTypedSeq TCError
e ([IllTypedInstr]
left [IllTypedInstr] -> [IllTypedInstr] -> [IllTypedInstr]
forall a. Semigroup a => a -> a -> a
<> (ExpandedOp -> IllTypedInstr) -> [ExpandedOp] -> [IllTypedInstr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map ExpandedOp -> IllTypedInstr
NonTypedInstr [ExpandedOp]
rest))
  where
    handleFirst :: SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
    handleFirst :: SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
handleFirst packedInstr :: SomeInstr inp
packedInstr@(HST inp
inputStack :/ SomeInstrOut inp
instrAndOutputStack) = do
      case SomeInstrOut inp
instrAndOutputStack of
        Instr inp out
instr ::: HST out
outputStack -> do
          TypeCheckedSeq out
nextPiece <- TcInstrHandler
-> [ExpandedOp]
-> HST out
-> TypeCheckInstrNoExcept (TypeCheckedSeq out)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment TcInstrHandler
tcInstr [ExpandedOp]
rest HST out
outputStack
          let combiner :: SomeInstr out -> SomeInstr inp
combiner = HST inp -> Instr inp out -> SomeInstr out -> SomeInstr inp
forall {inp :: [T]} {inp :: [T]}.
HST inp -> Instr inp inp -> SomeInstr inp -> SomeInstr inp
combine HST inp
inputStack Instr inp out
instr
          TypeCheckedSeq inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure case TypeCheckedSeq out
nextPiece of
            WellTypedSeq SomeInstr out
nextInstr -> SomeInstr inp -> TypeCheckedSeq inp
forall (inp :: [T]). SomeInstr inp -> TypeCheckedSeq inp
WellTypedSeq (SomeInstr out -> SomeInstr inp
combiner SomeInstr out
nextInstr)
            MixedSeq SomeInstr out
nextInstr TCError
err [IllTypedInstr]
left -> SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
forall (inp :: [T]).
SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
MixedSeq (SomeInstr out -> SomeInstr inp
combiner SomeInstr out
nextInstr) TCError
err [IllTypedInstr]
left
            IllTypedSeq TCError
err [IllTypedInstr]
left -> SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
forall (inp :: [T]).
SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
MixedSeq SomeInstr inp
packedInstr TCError
err [IllTypedInstr]
left
        AnyOutInstr{} -> TypeCheckedSeq inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure case [ExpandedOp]
rest of
          [] -> SomeInstr inp -> TypeCheckedSeq inp
forall (inp :: [T]). SomeInstr inp -> TypeCheckedSeq inp
WellTypedSeq SomeInstr inp
packedInstr
          ExpandedOp
op : [ExpandedOp]
ops -> (SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
forall (inp :: [T]).
SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
MixedSeq
                        SomeInstr inp
packedInstr
                        (ErrorSrcPos -> NonEmpty ExpandedOp -> TCError
TCUnreachableCode (ExpandedOp -> ErrorSrcPos
extractOpPos ExpandedOp
op) (ExpandedOp
op ExpandedOp -> [ExpandedOp] -> NonEmpty ExpandedOp
forall a. a -> [a] -> NonEmpty a
:| [ExpandedOp]
ops))
                        ((ExpandedOp -> IllTypedInstr) -> [ExpandedOp] -> [IllTypedInstr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map ExpandedOp -> IllTypedInstr
NonTypedInstr [ExpandedOp]
ops))

    combine :: HST inp -> Instr inp inp -> SomeInstr inp -> SomeInstr inp
combine HST inp
inp Instr inp inp
Nop (HST inp
_ :/ SomeInstrOut inp
nextPart) = HST inp
HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ SomeInstrOut inp
nextPart
    combine HST inp
inp Instr inp inp
i1 (HST inp
_ :/ SomeInstrOut inp
nextPart) = HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ (forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeInstrOut inp -> SomeInstrOut inp
forall (inp :: [T]) (inp' :: [T]).
(forall (out :: [T]). Instr inp out -> Instr inp' out)
-> SomeInstrOut inp -> SomeInstrOut 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) SomeInstrOut inp
nextPart

    extractOpPos :: Un.ExpandedOp -> ErrorSrcPos
    extractOpPos :: ExpandedOp -> ErrorSrcPos
extractOpPos (Un.WithSrcEx ErrorSrcPos
loc ExpandedOp
_) = ErrorSrcPos
loc
    extractOpPos ExpandedOp
_ = ErrorSrcPos
forall a. Default a => a
def

-- | Like 'typeCheckImpl' but without the first and the last stack type
-- comments. Useful to reduce duplication of stack type comments.
typeCheckImplStripped
  :: forall inp . SingI inp
  => TcInstrHandler
  -> [Un.ExpandedOp]
  -> HST inp
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplStripped :: forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplStripped TcInstrHandler
tcInstr [] HST inp
inp
  = TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment TcInstrHandler
tcInstr [] HST inp
inp
typeCheckImplStripped TcInstrHandler
tcInstr (ExpandedOp
op : [ExpandedOp]
ops) HST inp
inp = do
  TypeCheckedSeq inp
done <- TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op HST inp
inp
  TcInstrHandler
-> TypeCheckedSeq inp
-> [ExpandedOp]
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
TcInstrHandler
-> TypeCheckedSeq inp
-> [ExpandedOp]
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
continueTypeChecking TcInstrHandler
tcInstr TypeCheckedSeq inp
done [ExpandedOp]
ops

typeCheckImpl
  :: forall inp . SingI inp
  => TcInstrHandler
  -> [Un.ExpandedOp]
  -> HST inp
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl :: forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl TcInstrHandler
tcInstr [ExpandedOp]
ops HST inp
inputStack = do
  TypeCheckedSeq inp
tcSeq <- TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment TcInstrHandler
tcInstr [ExpandedOp]
ops HST inp
inputStack
  (SomeInstr inp
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
      (SomeInstr inp))
-> TypeCheckedSeq inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq inp)
forall (f :: * -> *) (inp :: [T]) (inp' :: [T]).
Applicative f =>
(SomeInstr inp -> f (SomeInstr inp'))
-> TypeCheckedSeq inp -> f (TypeCheckedSeq inp')
mapMSeq SomeInstr inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (SomeInstr inp)
forall {f :: * -> *} {inp :: [T]}.
MultiReader
  (MultiReaderDepth TypeCheckOptions (MultiReaderIso f))
  TypeCheckOptions
  f =>
SomeInstr inp -> f (SomeInstr inp)
appendTypeComment TypeCheckedSeq inp
tcSeq
  where
    appendTypeComment :: SomeInstr inp -> f (SomeInstr inp)
appendTypeComment packedI :: SomeInstr inp
packedI@(HST inp
inp :/ SomeInstrOut 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, SomeInstrOut inp
iAndOut) of
        (Bool
True, Instr inp out
i ::: HST out
out) -> HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr 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 -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST out
out
        (Bool
True, AnyOutInstr forall (out :: [T]). Instr inp out
i) -> HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ (forall (out :: [T]). Instr inp out) -> SomeInstrOut inp
forall (inp :: [T]).
(forall (out :: [T]). Instr inp out) -> SomeInstrOut 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, SomeInstrOut inp)
_ -> SomeInstr inp
packedI


prependStackTypeComment
  :: SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp)
prependStackTypeComment :: forall (inp :: [T]).
SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp)
prependStackTypeComment packedInstr :: SomeInstr inp
packedInstr@(HST inp
inp :/ SomeInstrOut inp
_) = do
  Bool
verbose <- (TypeCheckOptions -> Bool)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (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 (SomeInstr inp -> Bool
forall (inp :: [T]). SomeInstr inp -> Bool
isNop' SomeInstr inp
packedInstr))
    then (forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeInstr inp -> SomeInstr inp
forall (inp :: [T]).
(forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeInstr inp -> SomeInstr 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)) SomeInstr inp
packedInstr
    else SomeInstr inp
packedInstr

isNop' :: SomeInstr inp -> Bool
isNop' :: forall (inp :: [T]). SomeInstr 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
  => (SomeInstr inp -> f (SomeInstr inp'))
  -> TypeCheckedSeq inp
  -> f (TypeCheckedSeq inp')
mapMSeq :: forall (f :: * -> *) (inp :: [T]) (inp' :: [T]).
Applicative f =>
(SomeInstr inp -> f (SomeInstr inp'))
-> TypeCheckedSeq inp -> f (TypeCheckedSeq inp')
mapMSeq SomeInstr inp -> f (SomeInstr inp')
f TypeCheckedSeq inp
v = case TypeCheckedSeq inp
v of
  WellTypedSeq SomeInstr inp
instr -> SomeInstr inp -> f (SomeInstr inp')
f SomeInstr inp
instr f (SomeInstr inp')
-> (SomeInstr inp' -> TypeCheckedSeq inp')
-> f (TypeCheckedSeq inp')
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> SomeInstr inp' -> TypeCheckedSeq inp'
forall (inp :: [T]). SomeInstr inp -> TypeCheckedSeq inp
WellTypedSeq
  MixedSeq SomeInstr inp
instr TCError
err [IllTypedInstr]
tail' -> SomeInstr inp -> f (SomeInstr inp')
f SomeInstr inp
instr f (SomeInstr inp')
-> (SomeInstr inp' -> TypeCheckedSeq inp')
-> f (TypeCheckedSeq inp')
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \SomeInstr inp'
instr' -> SomeInstr inp' -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp'
forall (inp :: [T]).
SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
MixedSeq SomeInstr inp'
instr' TCError
err [IllTypedInstr]
tail'
  IllTypedSeq TCError
err [IllTypedInstr]
tail' -> TypeCheckedSeq inp' -> f (TypeCheckedSeq inp')
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq inp' -> f (TypeCheckedSeq inp'))
-> TypeCheckedSeq inp' -> f (TypeCheckedSeq inp')
forall a b. (a -> b) -> a -> b
$ TCError -> [IllTypedInstr] -> TypeCheckedSeq inp'
forall (inp :: [T]).
TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
IllTypedSeq TCError
err [IllTypedInstr]
tail'

mapSeq
  :: (SomeInstr inp -> SomeInstr inp')
  -> TypeCheckedSeq inp
  -> TypeCheckedSeq inp'
mapSeq :: forall (inp :: [T]) (inp' :: [T]).
(SomeInstr inp -> SomeInstr inp')
-> TypeCheckedSeq inp -> TypeCheckedSeq inp'
mapSeq SomeInstr inp -> SomeInstr inp'
f = Identity (TypeCheckedSeq inp') -> TypeCheckedSeq inp'
forall a. Identity a -> a
runIdentity (Identity (TypeCheckedSeq inp') -> TypeCheckedSeq inp')
-> (TypeCheckedSeq inp -> Identity (TypeCheckedSeq inp'))
-> TypeCheckedSeq inp
-> TypeCheckedSeq inp'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SomeInstr inp -> Identity (SomeInstr inp'))
-> TypeCheckedSeq inp -> Identity (TypeCheckedSeq inp')
forall (f :: * -> *) (inp :: [T]) (inp' :: [T]).
Applicative f =>
(SomeInstr inp -> f (SomeInstr inp'))
-> TypeCheckedSeq inp -> f (TypeCheckedSeq inp')
mapMSeq (SomeInstr inp' -> Identity (SomeInstr inp')
forall a. a -> Identity a
Identity (SomeInstr inp' -> Identity (SomeInstr inp'))
-> (SomeInstr inp -> SomeInstr inp')
-> SomeInstr inp
-> Identity (SomeInstr inp')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeInstr inp -> SomeInstr 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 inp -> TypeCheckedSeq inp
wrapWithLoc :: forall (inp :: [T]).
ErrorSrcPos -> TypeCheckedSeq inp -> TypeCheckedSeq inp
wrapWithLoc ErrorSrcPos
loc = (SomeInstr inp -> SomeInstr inp)
-> TypeCheckedSeq inp -> TypeCheckedSeq inp
forall (inp :: [T]) (inp' :: [T]).
(SomeInstr inp -> SomeInstr inp')
-> TypeCheckedSeq inp -> TypeCheckedSeq inp'
mapSeq ((SomeInstr inp -> SomeInstr inp)
 -> TypeCheckedSeq inp -> TypeCheckedSeq inp)
-> (SomeInstr inp -> SomeInstr inp)
-> TypeCheckedSeq inp
-> TypeCheckedSeq inp
forall a b. (a -> b) -> a -> b
$ \SomeInstr inp
someInstr -> case SomeInstr inp
someInstr of
  (HST inp
_ :/ WithLoc{} ::: HST out
_) -> SomeInstr inp
someInstr
  (HST inp
inp :/ Instr inp out
instr ::: HST out
out) -> HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr 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 -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST out
out
  (HST inp
inp :/ AnyOutInstr forall (out :: [T]). Instr inp out
instr) -> HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ ((forall (out :: [T]). Instr inp out) -> SomeInstrOut inp
forall (inp :: [T]).
(forall (out :: [T]). Instr inp out) -> SomeInstrOut inp
AnyOutInstr ((forall (out :: [T]). Instr inp out) -> SomeInstrOut inp)
-> (forall (out :: [T]). Instr inp out) -> SomeInstrOut 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 .
    ( MemOp c
    , SingI (MemOpKey c)
    , inp ~ (memKey : c : rs)
    , SingI rs
    , MonadReader TypeCheckInstrEnv m
    , MonadError TCError m
    )
  => HST inp
  -> VarAnn
  -> m (SomeInstr inp)
memImpl :: forall (c :: T) (memKey :: T) (rs :: [T]) (inp :: [T])
       (m :: * -> *).
(MemOp c, SingI (MemOpKey c), inp ~ (memKey : c : rs), SingI rs,
 MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
HST inp -> VarAnn -> m (SomeInstr 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 ->
      SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
inputHST HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr 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) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut 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 ->
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
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 :: ExpandedInstr
uInstr = VarAnn -> ExpandedInstr
forall op. VarAnn -> InstrAbstract op
Un.MEM VarAnn
varAnn

getImpl
  :: forall c getKey rs inp m .
    ( GetOp c, SingI (GetOpKey c)
    , WellTyped (GetOpVal c)
    , inp ~ (getKey : c : rs)
    , SingI rs
    , MonadReader TypeCheckInstrEnv m
    , MonadError TCError m
    )
  => HST inp
  -> SingT (GetOpVal c)
  -> VarAnn
  -> m (SomeInstr inp)
getImpl :: forall (c :: T) (getKey :: T) (rs :: [T]) (inp :: [T])
       (m :: * -> *).
(GetOp c, SingI (GetOpKey c), WellTyped (GetOpVal c),
 inp ~ (getKey : c : rs), SingI rs, MonadReader TypeCheckInstrEnv m,
 MonadError TCError m) =>
HST inp -> SingT (GetOpVal c) -> VarAnn -> m (SomeInstr 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 ->
      SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
inputHST HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr 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) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut 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 ->
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
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 :: ExpandedInstr
uInstr = VarAnn -> ExpandedInstr
forall op. VarAnn -> InstrAbstract op
Un.GET VarAnn
varAnn

updImpl
  :: forall c updKey updParams rs inp m .
    ( UpdOp c
    , SingI (UpdOpKey c), SingI (UpdOpParams c)
    , SingI rs
    , inp ~ (updKey : updParams : c : rs)
    , MonadReader TypeCheckInstrEnv m
    , MonadError TCError m
    )
  => HST inp
  -> VarAnn
  -> m (SomeInstr inp)
updImpl :: forall (c :: T) (updKey :: T) (updParams :: T) (rs :: [T])
       (inp :: [T]) (m :: * -> *).
(UpdOp c, SingI (UpdOpKey c), SingI (UpdOpParams c), SingI rs,
 inp ~ (updKey : updParams : c : rs),
 MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
HST inp -> VarAnn -> m (SomeInstr 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) ->
      SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
inputHST HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr 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) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut 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)
_) ->
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
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) ->
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
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 :: ExpandedInstr
uInstr = VarAnn -> ExpandedInstr
forall op. VarAnn -> InstrAbstract op
Un.UPDATE VarAnn
varAnn

getUpdImpl
  :: forall c updKey updParams rs inp m .
    ( 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 m
    )
  => HST inp
  -> VarAnn
  -> m (SomeInstr inp)
getUpdImpl :: forall (c :: T) (updKey :: T) (updParams :: T) (rs :: [T])
       (inp :: [T]) (m :: * -> *).
(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 m) =>
HST inp -> VarAnn -> m (SomeInstr 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) ->
      SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
inputHST HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr 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) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut 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))
_) ->
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
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) ->
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
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 :: ExpandedInstr
uInstr = VarAnn -> ExpandedInstr
forall op. VarAnn -> InstrAbstract op
Un.GET_AND_UPDATE VarAnn
varAnn

sizeImpl
  :: (SizeOp c, inp ~ (c ': rs), Monad m)
  => HST inp
  -> VarAnn
  -> m (SomeInstr inp)
sizeImpl :: forall (c :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(SizeOp c, inp ~ (c : rs), Monad m) =>
HST inp -> VarAnn -> m (SomeInstr inp)
sizeImpl i :: HST inp
i@((SingT x, Dict (WellTyped x))
_ ::& HST xs
rs) VarAnn
vn =
  SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr 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) -> SomeInstrOut (c : xs)
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut 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 (SomeInstr inp)
sliceImpl :: forall (c :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(SliceOp c, inp ~ ('TNat : 'TNat : c : rs), Monad m) =>
HST inp -> VarAnn -> m (SomeInstr 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
  SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr 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) -> SomeInstrOut ('TNat : 'TNat : c : xs)
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut 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 (SomeInstr inp)
concatImpl' :: forall (c :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(ConcatOp c, WellTyped c, inp ~ ('TList c : rs), Monad m) =>
HST inp -> VarAnn -> m (SomeInstr inp)
concatImpl' i :: HST inp
i@((STList Sing n
n, Dict (WellTyped x)
Dict) ::& HST xs
rs) VarAnn
vn = do
  SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr 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) -> SomeInstrOut ('TList c : xs)
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut 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 (SomeInstr 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 (SomeInstr inp)
concatImpl i :: HST inp
i@((SingT x
cn1, Dict (WellTyped x)
_) ::& (SingT x
_, Dict (WellTyped x)
_) ::& HST xs
rs) VarAnn
vn = do
  SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr 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) -> SomeInstrOut (x : x : xs)
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut 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.
     ( 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.ExpandedInstr
  -> t (SomeInstr inp)
arithImpl :: forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 ExpandedInstr
_ =
  SomeInstr inp -> t (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> t (SomeInstr inp))
-> SomeInstr inp -> t (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr 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) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut 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.
     ( Each '[SingI] [a, b]
     , inp ~ (a ': b ': rs)
     , SingI rs
     , MonadReader TypeCheckInstrEnv m
     , MonadError TCError m
     )
  => Sing a -> Sing b
  -> HST inp
  -> VarAnn
  -> Un.ExpandedInstr
  -> m (SomeInstr inp)
addImpl :: forall (a :: T) (b :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(Each '[SingI] '[a, b], inp ~ (a : b : rs), SingI rs,
 MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
Sing a
-> Sing b
-> HST inp
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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
_ ExpandedInstr
uInstr -> ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
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 (SomeInstr inp))
-> TCTypeError -> m (SomeInstr 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.
     ( SingI rs
     , Each '[SingI] [a, b]
     , inp ~ (a ': b ': rs)
     , MonadReader TypeCheckInstrEnv m
     , MonadError TCError m
     )
  => Sing a -> Sing b
  -> HST inp
  -> VarAnn
  -> Un.ExpandedInstr
  -> m (SomeInstr inp)
edivImpl :: forall (a :: T) (b :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(SingI rs, Each '[SingI] '[a, b], inp ~ (a : b : rs),
 MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
Sing a
-> Sing b
-> HST inp
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr 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 -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(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 -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
  (SingT a
STInt, SingT b
STNat) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(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 -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
  (SingT a
STNat, SingT b
STInt) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(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 -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
  (SingT a
STNat, SingT b
STNat) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(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 -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
  (SingT a
STMutez, SingT b
STMutez) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(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 -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
  (SingT a
STMutez, SingT b
STNat) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(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 -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
  (SingT a, SingT b)
_ -> \HST inp
i VarAnn
_ ExpandedInstr
uInstr -> ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
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 (SomeInstr inp))
-> TCTypeError -> m (SomeInstr 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.ExpandedInstr
  -> t (SomeInstr inp)
edivImplDo :: forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(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 -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo i :: HST inp
i@((SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
_ ::& HST xs
rs) VarAnn
vn ExpandedInstr
_ =
  SomeInstr inp -> t (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> t (SomeInstr inp))
-> SomeInstr inp -> t (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr 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)
-> SomeInstrOut (n : m : s)
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut 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.
     ( Each '[SingI] [a, b]
     , inp ~ (a ': b ': rs)
     , SingI rs
     , MonadReader TypeCheckInstrEnv m
     , MonadError TCError m
     )
  => Sing a -> Sing b
  -> HST inp
  -> VarAnn
  -> Un.ExpandedInstr
  -> m (SomeInstr inp)
subImpl :: forall (a :: T) (b :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(Each '[SingI] '[a, b], inp ~ (a : b : rs), SingI rs,
 MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
Sing a
-> Sing b
-> HST inp
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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
_ ExpandedInstr
uInstr -> ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
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 (SomeInstr inp))
-> TCTypeError -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$
    ExpandedInstr -> Text -> TCTypeError
InvalidInstruction ExpandedInstr
uInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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
_ ExpandedInstr
uInstr -> ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
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 (SomeInstr inp))
-> TCTypeError -> m (SomeInstr 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.
     ( Each '[SingI] [a, b]
     , inp ~ (a ': b ': rs)
     , SingI rs
     , MonadReader TypeCheckInstrEnv m
     , MonadError TCError m
     )
  => Sing a -> Sing b
  -> HST inp
  -> VarAnn
  -> Un.ExpandedInstr
  -> m (SomeInstr inp)
mulImpl :: forall (a :: T) (b :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(Each '[SingI] '[a, b], inp ~ (a : b : rs), SingI rs,
 MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
Sing a
-> Sing b
-> HST inp
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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 :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr 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
_ ExpandedInstr
uInstr -> ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
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 (SomeInstr inp))
-> TCTypeError -> m (SomeInstr 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 (SomeInstr 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 (SomeInstr inp)
unaryArithImpl Instr inp (UnaryArithRes aop n : s)
mkInstr i :: HST inp
i@((SingT x, Dict (WellTyped x))
_ ::& HST xs
rs) = do
  SomeInstr inp -> t (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> t (SomeInstr inp))
-> SomeInstr inp -> t (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr 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) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut 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 (SomeInstr 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 (SomeInstr inp)
unaryArithImplAnnotated Instr inp (UnaryArithRes aop n : s)
mkInstr i :: HST inp
i@((SingT x
n, Dict (WellTyped x)
_) ::& HST xs
rs) = do
  SomeInstr inp -> t (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> t (SomeInstr inp))
-> SomeInstr inp -> t (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ Instr inp (x : xs)
Instr inp (UnaryArithRes aop n : s)
mkInstr Instr inp (x : xs) -> HST (x : xs) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut 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)