-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

module Michelson.TypeCheck.Helpers
    ( deriveSpecialVN
    , deriveSpecialFNs
    , deriveVN
    , deriveNsOr
    , deriveNsOption
    , convergeHSTEl
    , convergeHST
    , hstToTs
    , eqHST
    , eqHST1
    , lengthHST

    , ensureDistinctAsc
    , eqType
    , onTypeCheckInstrAnnErr
    , onTypeCheckInstrErr
    , onScopeCheckInstrErr
    , typeCheckInstrErr
    , typeCheckInstrErr'
    , typeCheckImpl
    , typeCheckImplStripped
    , matchTypes

    , memImpl
    , getImpl
    , updImpl
    , sliceImpl
    , concatImpl
    , concatImpl'
    , sizeImpl
    , arithImpl
    , addImpl
    , subImpl
    , mulImpl
    , edivImpl
    , unaryArithImpl
    , unaryArithImplAnnotated
    , withCompareableCheck
    ) where

import Prelude hiding (EQ, GT, LT)

import Control.Monad.Except (MonadError, throwError)
import Data.Constraint (Dict(..), withDict)
import Data.Default (def)
import Data.Singletons (Sing, SingI(sing), demote)
import qualified Data.Text as T
import Data.Typeable ((:~:)(..), eqT)
import Fmt ((+||), (||+))

import Michelson.ErrorPos (InstrCallStack)
import Michelson.TypeCheck.Error (TCError(..), TCTypeError(..), TypeContext(..))
import Michelson.TypeCheck.TypeCheck
import Michelson.TypeCheck.Types
import Michelson.TypeCheck.TypeCheckedSeq (IllTypedInstr(..), TypeCheckedSeq(..))
import Michelson.Typed
  (BadTypeForScope(..), CommentType(StackTypeComment), Comparable, ExtInstr(COMMENT_ITEM),
  Instr(..), KnownT, Notes(..), PackedNotes(..), SingT(..), T(..), WellTyped, converge,
  getComparableProofS, notesT, orAnn, starNotes)
import Michelson.Typed.Annotation (AnnConvergeError, isStar)
import Michelson.Typed.Arith (Add, ArithOp(..), Mul, Sub, UnaryArithOp(..))
import Michelson.Typed.Polymorphic
  (ConcatOp, EDivOp(..), GetOp(..), MemOp(..), SizeOp, SliceOp, UpdOp(..))

import qualified Michelson.Untyped as Un
import Michelson.Untyped.Annotation (Annotation(..), FieldAnn, VarAnn, ann)
import Util.Type (onFirst)

-- | Function which derives special annotations
-- for PAIR instruction.
--
-- Namely, it does following transformation:
-- @
--  PAIR %@@ %@@ [ @@p.a int : @@p.b int : .. ]
--  ~
--  [ @@p (pair (int %a) (int %b) : .. ]
-- @
--
-- All relevant cases (e.g. @PAIR %myf %@@ @)
-- are handled as they should be according to spec.
deriveSpecialFNs
  :: FieldAnn -> FieldAnn
  -> VarAnn -> VarAnn
  -> (VarAnn, FieldAnn, FieldAnn)
deriveSpecialFNs :: FieldAnn
-> FieldAnn -> VarAnn -> VarAnn -> (VarAnn, FieldAnn, FieldAnn)
deriveSpecialFNs "@" "@" pvn :: VarAnn
pvn qvn :: VarAnn
qvn = (VarAnn
vn, FieldAnn
pfn, FieldAnn
qfn)
  where
    ps :: [Text]
ps = Text -> Text -> [Text]
T.splitOn "." (Text -> [Text]) -> Text -> [Text]
forall a b. (a -> b) -> a -> b
$ VarAnn -> Text
forall k (tag :: k). Annotation tag -> Text
unAnnotation VarAnn
pvn
    qs :: [Text]
qs = Text -> Text -> [Text]
T.splitOn "." (Text -> [Text]) -> Text -> [Text]
forall a b. (a -> b) -> a -> b
$ VarAnn -> Text
forall k (tag :: k). Annotation tag -> Text
unAnnotation VarAnn
qvn
    fns :: [Text]
fns = (Text, Text) -> Text
forall a b. (a, b) -> a
fst ((Text, Text) -> Text) -> [(Text, Text)] -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Text, Text) -> Bool) -> [(Text, Text)] -> [(Text, Text)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile ((Text -> Text -> Bool) -> (Text, Text) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
(==)) ([Text] -> [Text] -> [(Text, Text)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Text]
ps [Text]
qs)
    vn :: VarAnn
vn = Text -> VarAnn
forall k (a :: k). HasCallStack => Text -> Annotation a
ann (Text -> VarAnn) -> Text -> VarAnn
forall a b. (a -> b) -> a -> b
$ Text -> [Text] -> Text
T.intercalate "." [Text]
fns
    pfn :: FieldAnn
pfn = Text -> FieldAnn
forall k (a :: k). HasCallStack => Text -> Annotation a
ann (Text -> FieldAnn) -> Text -> FieldAnn
forall a b. (a -> b) -> a -> b
$ Text -> [Text] -> Text
T.intercalate "." ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ Int -> [Text] -> [Text]
forall a. Int -> [a] -> [a]
drop ([Text] -> Int
forall t. Container t => t -> Int
length [Text]
fns) [Text]
ps
    qfn :: FieldAnn
qfn = Text -> FieldAnn
forall k (a :: k). HasCallStack => Text -> Annotation a
ann (Text -> FieldAnn) -> Text -> FieldAnn
forall a b. (a -> b) -> a -> b
$ Text -> [Text] -> Text
T.intercalate "." ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ Int -> [Text] -> [Text]
forall a. Int -> [a] -> [a]
drop ([Text] -> Int
forall t. Container t => t -> Int
length [Text]
fns) [Text]
qs
deriveSpecialFNs "@" qfn :: FieldAnn
qfn pvn :: VarAnn
pvn _   = (VarAnn
forall a. Default a => a
def, VarAnn -> FieldAnn
forall k1 k2 (tag1 :: k1) (tag2 :: k2).
Annotation tag1 -> Annotation tag2
Un.convAnn VarAnn
pvn, FieldAnn
qfn)
deriveSpecialFNs pfn :: FieldAnn
pfn "@" _ qvn :: VarAnn
qvn   = (VarAnn
forall a. Default a => a
def, FieldAnn
pfn, VarAnn -> FieldAnn
forall k1 k2 (tag1 :: k1) (tag2 :: k2).
Annotation tag1 -> Annotation tag2
Un.convAnn VarAnn
qvn)
deriveSpecialFNs pfn :: FieldAnn
pfn qfn :: FieldAnn
qfn _ _     = (VarAnn
forall a. Default a => a
def, FieldAnn
pfn, FieldAnn
qfn)

-- | Function which derives special annotations
-- for CDR / CAR instructions.
deriveSpecialVN :: VarAnn -> FieldAnn -> VarAnn -> VarAnn
deriveSpecialVN :: VarAnn -> FieldAnn -> VarAnn -> VarAnn
deriveSpecialVN vn :: VarAnn
vn elFn :: FieldAnn
elFn pairVN :: VarAnn
pairVN
  | VarAnn
vn VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== "%" = FieldAnn -> VarAnn
forall k1 k2 (tag1 :: k1) (tag2 :: k2).
Annotation tag1 -> Annotation tag2
Un.convAnn FieldAnn
elFn
  | VarAnn
vn VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== "%%" Bool -> Bool -> Bool
&& FieldAnn
elFn FieldAnn -> FieldAnn -> Bool
forall a. Eq a => a -> a -> Bool
/= FieldAnn
forall a. Default a => a
def = VarAnn
pairVN VarAnn -> VarAnn -> VarAnn
forall a. Semigroup a => a -> a -> a
<> FieldAnn -> VarAnn
forall k1 k2 (tag1 :: k1) (tag2 :: k2).
Annotation tag1 -> Annotation tag2
Un.convAnn FieldAnn
elFn
  | Bool
otherwise = VarAnn
vn

-- | Append suffix to variable annotation (if it's not empty)
deriveVN :: VarAnn -> VarAnn -> VarAnn
deriveVN :: VarAnn -> VarAnn -> VarAnn
deriveVN suffix :: VarAnn
suffix vn :: VarAnn
vn = VarAnn -> VarAnn -> Bool -> VarAnn
forall a. a -> a -> Bool -> a
bool (VarAnn
suffix VarAnn -> VarAnn -> VarAnn
forall a. Semigroup a => a -> a -> a
<> VarAnn
vn) VarAnn
forall a. Default a => a
def (VarAnn
vn VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
forall a. Default a => a
def)

-- | Function which extracts annotations for @or@ type
-- (for left and right parts).
--
-- It extracts field/type annotations and also auto-generates variable
-- annotations if variable annotation is not provided as second argument.
deriveNsOr :: Notes ('TOr a b) -> VarAnn -> (Notes a, Notes b, VarAnn, VarAnn)
deriveNsOr :: Notes ('TOr a b) -> VarAnn -> (Notes a, Notes b, VarAnn, VarAnn)
deriveNsOr (NTOr _ afn :: FieldAnn
afn bfn :: FieldAnn
bfn an :: Notes p
an bn :: Notes q
bn) ovn :: VarAnn
ovn =
  let avn :: VarAnn
avn = VarAnn -> VarAnn -> VarAnn
deriveVN (FieldAnn -> VarAnn
forall k1 k2 (tag1 :: k1) (tag2 :: k2).
Annotation tag1 -> Annotation tag2
Un.convAnn FieldAnn
afn VarAnn -> VarAnn -> VarAnn
forall k (t :: k). Annotation t -> Annotation t -> Annotation t
`orAnn` "left") VarAnn
ovn
      bvn :: VarAnn
bvn = VarAnn -> VarAnn -> VarAnn
deriveVN (FieldAnn -> VarAnn
forall k1 k2 (tag1 :: k1) (tag2 :: k2).
Annotation tag1 -> Annotation tag2
Un.convAnn FieldAnn
bfn VarAnn -> VarAnn -> VarAnn
forall k (t :: k). Annotation t -> Annotation t -> Annotation t
`orAnn` "right") VarAnn
ovn
   in (Notes a
Notes p
an, Notes b
Notes q
bn, VarAnn
avn, VarAnn
bvn)

-- | Function which extracts annotations for @option t@ type.
--
-- It extracts field/type annotations and also auto-generates variable
-- annotation for @Some@ case if it is not provided as second argument.
deriveNsOption :: Notes ('TOption a) -> VarAnn -> (Notes a, VarAnn)
deriveNsOption :: Notes ('TOption a) -> VarAnn -> (Notes a, VarAnn)
deriveNsOption (NTOption _ an :: Notes t
an) ovn :: VarAnn
ovn =
  let avn :: VarAnn
avn = VarAnn -> VarAnn -> VarAnn
deriveVN "some" VarAnn
ovn
   in (Notes a
Notes t
an, VarAnn
avn)

convergeHSTEl
  :: (Notes t, Dict (WellTyped t), VarAnn)
  -> (Notes t, Dict (WellTyped t), VarAnn)
  -> Either AnnConvergeError (Notes t, Dict (WellTyped t), VarAnn)
convergeHSTEl :: (Notes t, Dict (WellTyped t), VarAnn)
-> (Notes t, Dict (WellTyped t), VarAnn)
-> Either AnnConvergeError (Notes t, Dict (WellTyped t), VarAnn)
convergeHSTEl (an :: Notes t
an, d :: Dict (WellTyped t)
d@Dict (WellTyped t)
Dict, avn :: VarAnn
avn) (bn :: Notes t
bn, _, bvn :: VarAnn
bvn) =
  (,,) (Notes t
 -> Dict (WellTyped t)
 -> VarAnn
 -> (Notes t, Dict (WellTyped t), VarAnn))
-> Either AnnConvergeError (Notes t)
-> Either
     AnnConvergeError
     (Dict (WellTyped t)
      -> VarAnn -> (Notes t, Dict (WellTyped t), VarAnn))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Notes t -> Notes t -> Either AnnConvergeError (Notes t)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes t
an Notes t
bn Either
  AnnConvergeError
  (Dict (WellTyped t)
   -> VarAnn -> (Notes t, Dict (WellTyped t), VarAnn))
-> Either AnnConvergeError (Dict (WellTyped t))
-> Either
     AnnConvergeError (VarAnn -> (Notes t, Dict (WellTyped t), VarAnn))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Dict (WellTyped t) -> Either AnnConvergeError (Dict (WellTyped t))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
d
      Either
  AnnConvergeError (VarAnn -> (Notes t, Dict (WellTyped t), VarAnn))
-> Either AnnConvergeError VarAnn
-> Either AnnConvergeError (Notes t, Dict (WellTyped t), VarAnn)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> VarAnn -> Either AnnConvergeError VarAnn
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarAnn -> VarAnn -> Bool -> VarAnn
forall a. a -> a -> Bool -> a
bool VarAnn
forall a. Default a => a
def VarAnn
avn (Bool -> VarAnn) -> Bool -> VarAnn
forall a b. (a -> b) -> a -> b
$ VarAnn
avn VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
bvn)

-- | Combine annotations from two given stack types
convergeHST :: HST ts -> HST ts -> Either AnnConvergeError (HST ts)
convergeHST :: HST ts -> HST ts -> Either AnnConvergeError (HST ts)
convergeHST SNil SNil = HST '[] -> Either AnnConvergeError (HST '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure HST '[]
SNil
convergeHST (a :: (Notes x, Dict (WellTyped x), VarAnn)
a ::& as :: HST xs
as) (b :: (Notes x, Dict (WellTyped x), VarAnn)
b ::& bs :: HST xs
bs) =
    ((Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs))
-> Either AnnConvergeError (Notes x, Dict (WellTyped x), VarAnn)
-> Either AnnConvergeError (HST xs)
-> Either AnnConvergeError (HST (x : xs))
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
(::&) ((Notes x, Dict (WellTyped x), VarAnn)
-> (Notes x, Dict (WellTyped x), VarAnn)
-> Either AnnConvergeError (Notes x, Dict (WellTyped x), VarAnn)
forall (t :: T).
(Notes t, Dict (WellTyped t), VarAnn)
-> (Notes t, Dict (WellTyped t), VarAnn)
-> Either AnnConvergeError (Notes t, Dict (WellTyped t), VarAnn)
convergeHSTEl (Notes x, Dict (WellTyped x), VarAnn)
a (Notes x, Dict (WellTyped x), VarAnn)
(Notes x, Dict (WellTyped x), VarAnn)
b) (HST xs -> HST xs -> Either AnnConvergeError (HST xs)
forall (ts :: [T]).
HST ts -> HST ts -> Either AnnConvergeError (HST ts)
convergeHST HST xs
as HST xs
HST xs
bs)

-- | Extract singleton for each single type of the given stack.
hstToTs :: HST st -> [T]
hstToTs :: HST st -> [T]
hstToTs = \case
  SNil -> []
  (notes :: Notes x
notes, _, _) ::& hst :: HST xs
hst -> Notes x -> T
forall (t :: T). SingI t => Notes t -> T
notesT Notes x
notes 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.
      (Typeable as, Typeable bs)
  => HST as -> HST bs -> Either TCTypeError (as :~: bs)
eqHST :: HST as -> HST bs -> Either TCTypeError (as :~: bs)
eqHST (HST as
hst :: HST xs) (HST bs
hst' :: HST ys) = do
  case (Typeable as, Typeable bs) => Maybe (as :~: bs)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @as @bs of
    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
$ [T] -> [T] -> TCTypeError
StackEqError (HST as -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST as
hst) (HST bs -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST bs
hst')
    Just Refl -> do
      Either TCTypeError (HST as) -> Either TCTypeError ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Either TCTypeError (HST as) -> Either TCTypeError ())
-> Either TCTypeError (HST as) -> Either TCTypeError ()
forall a b. (a -> b) -> a -> b
$ HST as -> HST as -> Either AnnConvergeError (HST as)
forall (ts :: [T]).
HST ts -> HST ts -> Either AnnConvergeError (HST ts)
convergeHST HST as
hst HST as
HST bs
hst' Either AnnConvergeError (HST as)
-> (AnnConvergeError -> TCTypeError) -> Either TCTypeError (HST as)
forall (p :: * -> * -> *) a c b.
Bifunctor p =>
p a c -> (a -> b) -> p b c
`onFirst` AnnConvergeError -> TCTypeError
AnnError
      return as :~: bs
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.
      (Typeable st, WellTyped t)
  => HST st -> Either TCTypeError (st :~: '[t])
eqHST1 :: HST st -> Either TCTypeError (st :~: '[t])
eqHST1 hst :: HST st
hst = do
  let hst' :: HST '[t]
hst' = SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @t Sing t -> HST '[] -> HST '[t]
forall (xs :: [T]) (x :: T).
(Typeable xs, WellTyped x) =>
Sing x -> HST xs -> HST (x : xs)
-:& HST '[]
SNil
  case (Typeable '[t], Typeable st) => Maybe ('[t] :~: st)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @'[t] @st of
    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
$ [T] -> [T] -> TCTypeError
StackEqError (HST '[t] -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST '[t]
hst') (HST st -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST st
hst)
    Just 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 :: HST xs -> Natural
lengthHST (_ ::& xs :: HST xs
xs) = 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 SNil = 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, Show a) => (a -> b) -> [a] -> Either Text [a]
ensureDistinctAsc :: (a -> b) -> [a] -> Either Text [a]
ensureDistinctAsc toCmp :: a -> b
toCmp = \case
  (e1 :: a
e1 : e2 :: a
e2 : l :: [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, Show 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
$ "Entries are unordered (" Builder -> Builder -> Text
forall b. FromBuilder b => Builder -> Builder -> b
+|| a
e1 a -> Builder -> Builder
forall a b. (Show a, FromBuilder b) => a -> Builder -> b
||+ " >= " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+|| a
e2 a -> Builder -> Builder
forall a b. (Show a, FromBuilder b) => a -> Builder -> b
||+ ")"
  l :: [a]
l -> [a] -> Either Text [a]
forall a b. b -> Either a b
Right [a]
l

-- | Function @eqType@ is a simple wrapper around @Data.Typeable.eqT@ suited
-- for use within @Either TCTypeError a@ applicative.
eqType
  :: forall (a :: T) (b :: T).
      (Each '[KnownT] [a, b])
  => Either TCTypeError (a :~: b)
eqType :: Either TCTypeError (a :~: b)
eqType = Either TCTypeError (a :~: b)
-> ((a :~: b) -> Either TCTypeError (a :~: b))
-> Maybe (a :~: b)
-> Either TCTypeError (a :~: b)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TCTypeError -> Either TCTypeError (a :~: b)
forall a b. a -> Either a b
Left (TCTypeError -> Either TCTypeError (a :~: b))
-> TCTypeError -> Either TCTypeError (a :~: b)
forall a b. (a -> b) -> a -> b
$ T -> T -> TCTypeError
TypeEqError ((SingKind T, SingI a) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @a) ((SingKind T, SingI b) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @b)) (a :~: b) -> Either TCTypeError (a :~: b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (a :~: b)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT

onTypeCheckInstrErr
  :: (MonadReader InstrCallStack m, MonadError TCError m)
  => Un.ExpandedInstr -> SomeHST -> Maybe TypeContext
  -> Either TCTypeError a -> m a
onTypeCheckInstrErr :: ExpandedInstr
-> SomeHST -> Maybe TypeContext -> Either TCTypeError a -> m a
onTypeCheckInstrErr instr :: ExpandedInstr
instr hst :: SomeHST
hst mContext :: Maybe TypeContext
mContext ei :: 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 InstrCallStack 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 InstrCallStack m, MonadError TCError m, SingI t)
  => Un.ExpandedInstr -> SomeHST -> Maybe TypeContext
  -> Either BadTypeForScope a -> m a
onScopeCheckInstrErr :: ExpandedInstr
-> SomeHST -> Maybe TypeContext -> Either BadTypeForScope a -> m a
onScopeCheckInstrErr instr :: ExpandedInstr
instr hst :: SomeHST
hst mContext :: Maybe TypeContext
mContext = \case
  Right a :: a
a -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
  Left e :: BadTypeForScope
e -> do
    InstrCallStack
pos <- m InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
    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
-> InstrCallStack
-> Maybe TypeContext
-> Maybe TCTypeError
-> TCError
TCFailedOnInstr ExpandedInstr
instr SomeHST
hst InstrCallStack
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 ((SingKind T, SingI t) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @t) BadTypeForScope
e

typeCheckInstrErr
  :: (MonadReader InstrCallStack m, MonadError TCError m)
  => Un.ExpandedInstr -> SomeHST -> Maybe TypeContext
  -> m a
typeCheckInstrErr :: ExpandedInstr -> SomeHST -> Maybe TypeContext -> m a
typeCheckInstrErr instr :: ExpandedInstr
instr hst :: SomeHST
hst mContext :: Maybe TypeContext
mContext = do
  InstrCallStack
pos <- m InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
  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
-> InstrCallStack
-> Maybe TypeContext
-> Maybe TCTypeError
-> TCError
TCFailedOnInstr ExpandedInstr
instr SomeHST
hst InstrCallStack
pos Maybe TypeContext
mContext Maybe TCTypeError
forall a. Maybe a
Nothing

typeCheckInstrErr'
  :: (MonadReader InstrCallStack m, MonadError TCError m)
  => Un.ExpandedInstr -> SomeHST -> Maybe TypeContext
  -> TCTypeError -> m a
typeCheckInstrErr' :: ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' instr :: ExpandedInstr
instr hst :: SomeHST
hst mContext :: Maybe TypeContext
mContext err :: TCTypeError
err = do
  InstrCallStack
pos <- m InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
  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
-> InstrCallStack
-> Maybe TypeContext
-> Maybe TCTypeError
-> TCError
TCFailedOnInstr ExpandedInstr
instr SomeHST
hst InstrCallStack
pos Maybe TypeContext
mContext (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just TCTypeError
err)

onTypeCheckInstrAnnErr
  :: (MonadReader InstrCallStack m, MonadError TCError m, Typeable ts)
  => Un.ExpandedInstr -> HST ts -> Maybe TypeContext
  -> Either AnnConvergeError a -> m a
onTypeCheckInstrAnnErr :: ExpandedInstr
-> HST ts -> Maybe TypeContext -> Either AnnConvergeError a -> m a
onTypeCheckInstrAnnErr instr :: ExpandedInstr
instr i :: HST ts
i mContext :: Maybe TypeContext
mContext ei :: Either AnnConvergeError a
ei =
  ExpandedInstr
-> SomeHST -> Maybe TypeContext -> Either TCTypeError a -> m a
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr
-> SomeHST -> Maybe TypeContext -> Either TCTypeError a -> m a
onTypeCheckInstrErr ExpandedInstr
instr (HST ts -> SomeHST
forall (ts :: [T]). Typeable ts => HST ts -> SomeHST
SomeHST HST ts
i) Maybe TypeContext
mContext (Either AnnConvergeError a
ei Either AnnConvergeError a
-> (AnnConvergeError -> TCTypeError) -> Either TCTypeError a
forall (p :: * -> * -> *) a c b.
Bifunctor p =>
p a c -> (a -> b) -> p b c
`onFirst` AnnConvergeError -> TCTypeError
AnnError)

withCompareableCheck
  :: forall a m v ts. (Typeable ts, MonadReader InstrCallStack m, MonadError TCError m)
  => Sing a
  -> Un.ExpandedInstr
  -> HST ts
  -> (Comparable a => v)
  -> m v
withCompareableCheck :: Sing a -> ExpandedInstr -> HST ts -> (Comparable a => v) -> m v
withCompareableCheck sng :: Sing a
sng instr :: ExpandedInstr
instr i :: HST ts
i act :: 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
  Nothing -> ExpandedInstr -> SomeHST -> Maybe TypeContext -> m v
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> m a
typeCheckInstrErr ExpandedInstr
instr (HST ts -> SomeHST
forall (ts :: [T]). Typeable 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. Typeable inp
  => TcInstrHandler
  -> Un.ExpandedOp
  -> HST inp
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl :: TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl tcInstr :: TcInstrHandler
tcInstr op' :: ExpandedOp
op' inputStack :: HST inp
inputStack = case ExpandedOp
op' of
  Un.WithSrcEx _ op :: ExpandedOp
op@Un.WithSrcEx{} -> TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
Typeable inp =>
TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op HST inp
inputStack
  Un.WithSrcEx loc :: InstrCallStack
loc (Un.PrimEx op :: ExpandedInstr
op)  -> InstrCallStack
-> ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrimWithLoc InstrCallStack
loc ExpandedInstr
op
  Un.WithSrcEx loc :: InstrCallStack
loc (Un.SeqEx sq :: [ExpandedOp]
sq)   -> InstrCallStack
-> [ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeqWithLoc InstrCallStack
loc [ExpandedOp]
sq
  Un.PrimEx op :: ExpandedInstr
op                     -> ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrim ExpandedInstr
op
  Un.SeqEx sq :: [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 :: InstrCallStack -> Un.ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
    typeCheckPrimWithLoc :: InstrCallStack
-> ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrimWithLoc loc :: InstrCallStack
loc op :: ExpandedInstr
op = (InstrCallStack -> InstrCallStack)
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (InstrCallStack -> InstrCallStack -> InstrCallStack
forall a b. a -> b -> a
const InstrCallStack
loc)
      (InstrCallStack -> TypeCheckedSeq inp -> TypeCheckedSeq inp
forall (inp :: [T]).
InstrCallStack -> TypeCheckedSeq inp -> TypeCheckedSeq inp
wrapWithLoc InstrCallStack
loc (TypeCheckedSeq inp -> TypeCheckedSeq inp)
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> TypeCheckInstrNoExcept (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 op :: ExpandedInstr
op = ExpandedInstr
-> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
TcInstrHandler
tcInstr ExpandedInstr
op HST inp
inputStack TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> (TypeCheckedSeq inp -> TypeCheckedSeq inp)
-> TypeCheckInstrNoExcept (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 SomeInstr inp -> SomeInstr inp
addNotes

    typeCheckSeqWithLoc :: InstrCallStack -> [Un.ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
    typeCheckSeqWithLoc :: InstrCallStack
-> [ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeqWithLoc loc :: InstrCallStack
loc = (TypeCheckedSeq inp -> TypeCheckedSeq inp)
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (InstrCallStack -> TypeCheckedSeq inp -> TypeCheckedSeq inp
forall (inp :: [T]).
InstrCallStack -> TypeCheckedSeq inp -> TypeCheckedSeq inp
wrapWithLoc InstrCallStack
loc) (TypeCheckInstrNoExcept (TypeCheckedSeq inp)
 -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> ([ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> [ExpandedOp]
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InstrCallStack -> InstrCallStack)
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (InstrCallStack -> InstrCallStack -> InstrCallStack
forall a b. a -> b -> a
const InstrCallStack
loc) (TypeCheckInstrNoExcept (TypeCheckedSeq inp)
 -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> ([ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> [ExpandedOp]
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeq

    typeCheckSeq :: [Un.ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
    typeCheckSeq :: [ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeq sq :: [ExpandedOp]
sq = TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
Typeable inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl TcInstrHandler
tcInstr [ExpandedOp]
sq HST inp
inputStack
                  TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> (TypeCheckedSeq inp -> TypeCheckedSeq inp)
-> TypeCheckInstrNoExcept (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 (SomeInstr inp -> SomeInstr inp
addNotes (SomeInstr inp -> SomeInstr inp)
-> (SomeInstr inp -> SomeInstr inp)
-> SomeInstr inp
-> SomeInstr inp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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)

    addNotes :: SomeInstr inp -> SomeInstr inp
    addNotes :: SomeInstr inp -> SomeInstr inp
addNotes (inp :: HST inp
inp :/ i :: Instr inp out
i ::: out :: HST out
out) = HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ HST out -> Instr inp out -> Instr inp out
forall (d :: [T]) (c :: [T]). HST d -> Instr c d -> Instr c d
wrapWithNotes HST out
out Instr inp out
i Instr inp out -> HST out -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST out
out
    addNotes i :: SomeInstr inp
i = SomeInstr inp
i

    wrapWithNotes :: HST d -> Instr c d -> Instr c d
    wrapWithNotes :: HST d -> Instr c d -> Instr c d
wrapWithNotes outputStack :: HST d
outputStack instr :: Instr c d
instr = case Instr c d
instr of
      -- Abstractions for instructions:
      Nop -> Instr c d
instr'
      Seq _ _ -> Instr c d
instr'
      Nested _ -> Instr c d
instr'
      DocGroup _ _ -> Instr c d
instr'
      Ext _ -> Instr c d
instr'
      FrameInstr _ _ -> Instr c d
instr'
      WithLoc _ _ -> Instr c d
instr'
      -- These two shouldn't happen, since annotations are added here.
      InstrWithNotes _ _ -> Instr c d
instr'
      InstrWithVarNotes _ _ -> Instr c d
instr'

      -- Instructions that don't produce notes:
      DROP -> Instr c d
instr'
      SWAP -> Instr c d
instr'
      DIG _ -> Instr c d
instr'
      DUG _ -> Instr c d
instr'
      IF_NONE _ _ -> Instr c d
instr'
      IF_LEFT _ _ -> Instr c d
instr'
      IF_CONS _ _ -> Instr c d
instr'
      ITER _ -> Instr c d
instr'
      IF _ _ -> Instr c d
instr'
      LOOP _ -> Instr c d
instr'
      LOOP_LEFT _ -> Instr c d
instr'
      DIP _ -> Instr c d
instr'
      DIPN _ _ -> Instr c d
instr'
      FAILWITH -> Instr c d
instr'

      -- Instructions that produce at most two notes:
      CREATE_CONTRACT _ -> case HST d
outputStack of
        ((np :: Notes x
np, _, vp :: VarAnn
vp) ::& (_, _, vs :: VarAnn
vs) ::& _) ->
          let withNotes :: Instr c (x : 'TAddress : s) -> Instr c (x : 'TAddress : s)
withNotes = if Notes x -> Bool
forall (t :: T). SingI t => Notes t -> Bool
isStar Notes x
np then Instr c (x : 'TAddress : s) -> Instr c (x : 'TAddress : s)
forall a. a -> a
id else PackedNotes (x : 'TAddress : s)
-> Instr c (x : 'TAddress : s) -> Instr c (x : 'TAddress : s)
forall (b :: [T]) (a :: [T]).
PackedNotes b -> Instr a b -> Instr a b
InstrWithNotes (Notes x -> PackedNotes (x : 'TAddress : s)
forall (a :: T) (s :: [T]).
SingI a =>
Notes a -> PackedNotes (a : s)
PackedNotes Notes x
np)
              withVarNotes :: Instr c (x : 'TAddress : s) -> Instr c (x : 'TAddress : s)
withVarNotes = if VarAnn
vp VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
forall k (a :: k). Annotation a
Un.noAnn Bool -> Bool -> Bool
&& VarAnn
vs VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
forall k (a :: k). Annotation a
Un.noAnn then Instr c (x : 'TAddress : s) -> Instr c (x : 'TAddress : s)
forall a. a -> a
id else NonEmpty VarAnn
-> Instr c (x : 'TAddress : s) -> Instr c (x : 'TAddress : s)
forall (a :: [T]) (b :: [T]).
NonEmpty VarAnn -> Instr a b -> Instr a b
InstrWithVarNotes (VarAnn
vp VarAnn -> [VarAnn] -> NonEmpty VarAnn
forall a. a -> [a] -> NonEmpty a
:| [VarAnn
vs])
           in Instr c (x : 'TAddress : s) -> Instr c (x : 'TAddress : s)
withNotes (Instr c (x : 'TAddress : s) -> Instr c (x : 'TAddress : s))
-> (Instr c (x : 'TAddress : s) -> Instr c (x : 'TAddress : s))
-> Instr c (x : 'TAddress : s)
-> Instr c (x : 'TAddress : s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr c (x : 'TAddress : s) -> Instr c (x : 'TAddress : s)
withVarNotes (Instr c (x : 'TAddress : s) -> Instr c d)
-> Instr c (x : 'TAddress : s) -> Instr c d
forall a b. (a -> b) -> a -> b
$ Instr c d
Instr c (x : 'TAddress : s)
instr

      -- Instructions that produce at most one note:
      _ -> case HST d
outputStack of
        ((n :: Notes x
n, _, v :: VarAnn
v) ::& _) ->
          let withNotes :: Instr c (x : xs) -> Instr c (x : xs)
withNotes = if Notes x -> Bool
forall (t :: T). SingI t => Notes t -> Bool
isStar Notes x
n then Instr c (x : xs) -> Instr c (x : xs)
forall a. a -> a
id else PackedNotes (x : xs) -> Instr c (x : xs) -> Instr c (x : xs)
forall (b :: [T]) (a :: [T]).
PackedNotes b -> Instr a b -> Instr a b
InstrWithNotes (Notes x -> PackedNotes (x : xs)
forall (a :: T) (s :: [T]).
SingI a =>
Notes a -> PackedNotes (a : s)
PackedNotes Notes x
n)
              withVarNotes :: Instr c (x : xs) -> Instr c (x : xs)
withVarNotes = if VarAnn
v VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
forall k (a :: k). Annotation a
Un.noAnn then Instr c (x : xs) -> Instr c (x : xs)
forall a. a -> a
id else NonEmpty VarAnn -> Instr c (x : xs) -> Instr c (x : xs)
forall (a :: [T]) (b :: [T]).
NonEmpty VarAnn -> Instr a b -> Instr a b
InstrWithVarNotes (OneItem (NonEmpty VarAnn) -> NonEmpty VarAnn
forall x. One x => OneItem x -> x
one OneItem (NonEmpty VarAnn)
VarAnn
v)
           in Instr c (x : xs) -> Instr c (x : xs)
withNotes (Instr c (x : xs) -> Instr c (x : xs))
-> (Instr c (x : xs) -> Instr c (x : xs))
-> Instr c (x : xs)
-> Instr c (x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr c (x : xs) -> Instr c (x : xs)
withVarNotes (Instr c (x : xs) -> Instr c d) -> Instr c (x : xs) -> Instr c d
forall a b. (a -> b) -> a -> b
$ Instr c d
Instr c (x : xs)
instr
        SNil -> Instr c d
instr
      where
        instr' :: Instr c d
instr' = HST d -> Instr c d -> Instr c d
forall (d :: [T]) (c :: [T]). HST d -> Instr c d -> Instr c d
addNotesNoVarAnn HST d
outputStack Instr c d
instr

    addNotesNoVarAnn :: HST d -> Instr c d -> Instr c d
    addNotesNoVarAnn :: HST d -> Instr c d -> Instr c d
addNotesNoVarAnn outputStack :: HST d
outputStack instr :: Instr c d
instr = case HST d
outputStack of
      ((n :: Notes x
n, _, _) ::& _)
        | Notes x -> Bool
forall (t :: T). SingI t => Notes t -> Bool
isStar Notes x
n -> Instr c d
instr
        | Bool
otherwise -> PackedNotes (x : xs) -> Instr c (x : xs) -> Instr c (x : xs)
forall (b :: [T]) (a :: [T]).
PackedNotes b -> Instr a b -> Instr a b
InstrWithNotes (Notes x -> PackedNotes (x : xs)
forall (a :: T) (s :: [T]).
SingI a =>
Notes a -> PackedNotes (a : s)
PackedNotes Notes x
n) Instr c d
Instr c (x : xs)
instr
      SNil -> Instr c d
instr

-- | Like 'typeCheckImpl' but doesn't add a stack type comment after the
-- sequence.
typeCheckImplNoLastTypeComment
  :: forall inp . Typeable inp
  => TcInstrHandler
  -> [Un.ExpandedOp]
  -> HST inp
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment :: TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment _ [] inputStack :: HST inp
inputStack
  = TypeCheckedSeq inp -> TypeCheckInstrNoExcept (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 (s :: [T]). Instr s s
Nop Instr inp inp -> HST inp -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST inp
inputStack))
typeCheckImplNoLastTypeComment tcInstr :: TcInstrHandler
tcInstr [op :: ExpandedOp
op] inputStack :: HST inp
inputStack = do
  TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
Typeable inp =>
TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op HST inp
inputStack
      TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> (TypeCheckedSeq inp
    -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (SomeInstr inp
 -> ReaderT InstrCallStack TypeCheckNoExcept (SomeInstr inp))
-> TypeCheckedSeq inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (f :: * -> *) (inp :: [T]) (inp' :: [T]).
Applicative f =>
(SomeInstr inp -> f (SomeInstr inp'))
-> TypeCheckedSeq inp -> f (TypeCheckedSeq inp')
mapMSeq SomeInstr inp
-> ReaderT InstrCallStack TypeCheckNoExcept (SomeInstr inp)
forall (inp :: [T]).
SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp)
prependStackTypeComment
typeCheckImplNoLastTypeComment tcInstr :: TcInstrHandler
tcInstr (op :: ExpandedOp
op : ops :: [ExpandedOp]
ops) inputStack :: HST inp
inputStack = do
  TypeCheckedSeq inp
done <- TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
Typeable inp =>
TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op HST inp
inputStack
      TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> (TypeCheckedSeq inp
    -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (SomeInstr inp
 -> ReaderT InstrCallStack TypeCheckNoExcept (SomeInstr inp))
-> TypeCheckedSeq inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (f :: * -> *) (inp :: [T]) (inp' :: [T]).
Applicative f =>
(SomeInstr inp -> f (SomeInstr inp'))
-> TypeCheckedSeq inp -> f (TypeCheckedSeq inp')
mapMSeq SomeInstr inp
-> ReaderT InstrCallStack TypeCheckNoExcept (SomeInstr inp)
forall (inp :: [T]).
SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp)
prependStackTypeComment
  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

continueTypeChecking
  :: forall inp. ()
  => TcInstrHandler
  -> TypeCheckedSeq inp
  -> [Un.ExpandedOp]
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
continueTypeChecking :: TcInstrHandler
-> TypeCheckedSeq inp
-> [ExpandedOp]
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
continueTypeChecking tcInstr :: TcInstrHandler
tcInstr done :: TypeCheckedSeq inp
done rest :: [ExpandedOp]
rest = case TypeCheckedSeq inp
done of
  WellTypedSeq instr :: SomeInstr inp
instr -> SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
handleFirst SomeInstr inp
instr
  MixedSeq i :: SomeInstr inp
i e :: TCError
e left :: [IllTypedInstr]
left -> TypeCheckedSeq inp -> TypeCheckInstrNoExcept (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 e :: TCError
e left :: [IllTypedInstr]
left -> TypeCheckedSeq inp -> TypeCheckInstrNoExcept (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@(inputStack :: HST inp
inputStack :/ instrAndOutputStack :: SomeInstrOut inp
instrAndOutputStack) = do
      case SomeInstrOut inp
instrAndOutputStack of
        instr :: Instr inp out
instr ::: outputStack :: HST out
outputStack -> do
          TypeCheckedSeq out
nextPiece <- TcInstrHandler
-> [ExpandedOp]
-> HST out
-> TypeCheckInstrNoExcept (TypeCheckedSeq out)
forall (inp :: [T]).
Typeable 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]) (out :: [T]).
HST inp -> Instr inp out -> SomeInstr out -> SomeInstr inp
combine HST inp
inputStack Instr inp out
instr
          TypeCheckedSeq inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure case TypeCheckedSeq out
nextPiece of
            WellTypedSeq nextInstr :: SomeInstr out
nextInstr -> SomeInstr inp -> TypeCheckedSeq inp
forall (inp :: [T]). SomeInstr inp -> TypeCheckedSeq inp
WellTypedSeq (SomeInstr out -> SomeInstr inp
combiner SomeInstr out
nextInstr)
            MixedSeq nextInstr :: SomeInstr out
nextInstr err :: TCError
err left :: [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 err :: TCError
err left :: [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 -> TypeCheckInstrNoExcept (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
          op :: ExpandedOp
op : ops :: [ExpandedOp]
ops -> (SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
forall (inp :: [T]).
SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
MixedSeq
                        SomeInstr inp
packedInstr
                        (InstrCallStack -> NonEmpty ExpandedOp -> TCError
TCUnreachableCode (ExpandedOp -> InstrCallStack
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 out -> SomeInstr out -> SomeInstr inp
combine inp :: HST inp
inp Nop (_ :/ nextPart) = HST out
HST inp
inp HST out -> SomeInstrOut out -> SomeInstr out
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ SomeInstrOut out
nextPart
    combine inp :: HST inp
inp i1 :: Instr inp out
i1 (_ :/ nextPart :: SomeInstrOut out
nextPart) = HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ (forall (out :: [T]). Instr out out -> Instr inp out)
-> SomeInstrOut out -> SomeInstrOut inp
forall (inp :: [T]) (inp' :: [T]).
(forall (out :: [T]). Instr inp out -> Instr inp' out)
-> SomeInstrOut inp -> SomeInstrOut inp'
mapSomeInstrOut (Instr inp out -> Instr out out -> Instr inp out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr inp out
i1) SomeInstrOut out
nextPart

    extractOpPos :: Un.ExpandedOp -> InstrCallStack
    extractOpPos :: ExpandedOp -> InstrCallStack
extractOpPos (Un.WithSrcEx loc :: InstrCallStack
loc _) = InstrCallStack
loc
    extractOpPos _ = InstrCallStack
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 . Typeable inp
  => TcInstrHandler
  -> [Un.ExpandedOp]
  -> HST inp
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplStripped :: TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplStripped tcInstr :: TcInstrHandler
tcInstr [] inp :: HST inp
inp
  = TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
Typeable inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment TcInstrHandler
tcInstr [] HST inp
inp
typeCheckImplStripped tcInstr :: TcInstrHandler
tcInstr (op :: ExpandedOp
op : ops :: [ExpandedOp]
ops) inp :: HST inp
inp = do
  TypeCheckedSeq inp
done <- TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
Typeable 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 . Typeable inp
  => TcInstrHandler
  -> [Un.ExpandedOp]
  -> HST inp
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl :: TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl tcInstr :: TcInstrHandler
tcInstr ops :: [ExpandedOp]
ops inputStack :: HST inp
inputStack = do
  TypeCheckedSeq inp
tcSeq <- TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
Typeable inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment TcInstrHandler
tcInstr [ExpandedOp]
ops HST inp
inputStack
  (SomeInstr inp
 -> ReaderT InstrCallStack TypeCheckNoExcept (SomeInstr inp))
-> TypeCheckedSeq inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (f :: * -> *) (inp :: [T]) (inp' :: [T]).
Applicative f =>
(SomeInstr inp -> f (SomeInstr inp'))
-> TypeCheckedSeq inp -> f (TypeCheckedSeq inp')
mapMSeq SomeInstr inp
-> ReaderT InstrCallStack TypeCheckNoExcept (SomeInstr inp)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (inp :: [T]).
(MonadTrans t, MonadReader TypeCheckOptions m, Functor (t m)) =>
SomeInstr inp -> t m (SomeInstr inp)
appendTypeComment TypeCheckedSeq inp
tcSeq
  where
    appendTypeComment :: SomeInstr inp -> t m (SomeInstr inp)
appendTypeComment packedI :: SomeInstr inp
packedI@(inp :: HST inp
inp :/ iAndOut :: SomeInstrOut inp
iAndOut) = do
      Bool
verbose <- m Bool -> t m Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ((TypeCheckOptions -> Bool) -> m Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TypeCheckOptions -> Bool
tcVerbose)
      pure case (Bool
verbose, SomeInstrOut inp
iAndOut) of
        (True, i :: Instr inp out
i ::: out :: 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 (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
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]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST out
out
        (True, AnyOutInstr i :: 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 (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr inp out
forall (out :: [T]). Instr inp out
i Instr out out
forall (s :: [T]). Instr s s
noStackTypeComment)
        _ -> SomeInstr inp
packedI


prependStackTypeComment
  :: SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp)
prependStackTypeComment :: SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp)
prependStackTypeComment packedInstr :: SomeInstr inp
packedInstr@(inp :: HST inp
inp :/ _) = do
  Bool
verbose <- TypeCheckNoExcept Bool
-> ReaderT InstrCallStack TypeCheckNoExcept Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ((TypeCheckOptions -> Bool) -> TypeCheckNoExcept Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TypeCheckOptions -> Bool
tcVerbose)
  pure if Bool
verbose Bool -> Bool -> Bool
&& (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 (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
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' :: SomeInstr inp -> Bool
isNop' (_ :/ i :: Instr inp out
i ::: _) = Instr inp out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp out
i
isNop' (_ :/ AnyOutInstr i :: 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 :: Instr inp out -> Bool
isNop (WithLoc _ i :: Instr inp out
i) = Instr inp out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp out
i
isNop (InstrWithNotes _ i :: Instr inp out
i) = Instr inp out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp out
i
isNop (InstrWithVarNotes _ i :: Instr inp out
i) = Instr inp out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp out
i
isNop (FrameInstr _ i :: Instr a b
i) = Instr a b -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr a b
i
isNop (Seq i1 :: Instr inp b
i1 i2 :: 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
&& Instr b out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr b out
i2
isNop (Nested i :: Instr inp out
i) = Instr inp out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp out
i
isNop Nop = Bool
True
isNop (Ext _) = Bool
True
isNop _ = Bool
False

mapMSeq
  :: Applicative f
  => (SomeInstr inp -> f (SomeInstr inp'))
  -> TypeCheckedSeq inp
  -> f (TypeCheckedSeq inp')
mapMSeq :: (SomeInstr inp -> f (SomeInstr inp'))
-> TypeCheckedSeq inp -> f (TypeCheckedSeq inp')
mapMSeq f :: SomeInstr inp -> f (SomeInstr inp')
f v :: TypeCheckedSeq inp
v = case TypeCheckedSeq inp
v of
  WellTypedSeq instr :: 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 instr :: SomeInstr inp
instr err :: TCError
err tail' :: [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
<&> \instr' :: 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 err :: TCError
err tail' :: [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 :: (SomeInstr inp -> SomeInstr inp')
-> TypeCheckedSeq inp -> TypeCheckedSeq inp'
mapSeq f :: 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 :: HST st -> Instr st st
stackTypeComment = ExtInstr st -> Instr st st
forall (s :: [T]). ExtInstr s -> Instr s s
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 :: Instr st st
noStackTypeComment = ExtInstr st -> Instr st st
forall (s :: [T]). ExtInstr s -> Instr s s
Ext (CommentType -> ExtInstr st
forall (s :: [T]). CommentType -> ExtInstr s
COMMENT_ITEM (Maybe [T] -> CommentType
StackTypeComment Maybe [T]
forall a. Maybe a
Nothing))

wrapWithLoc :: InstrCallStack -> TypeCheckedSeq inp -> TypeCheckedSeq inp
wrapWithLoc :: InstrCallStack -> TypeCheckedSeq inp -> TypeCheckedSeq inp
wrapWithLoc loc :: InstrCallStack
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 :: SomeInstr inp
someInstr -> case SomeInstr inp
someInstr of
  (_ :/ WithLoc{} ::: _) -> SomeInstr inp
someInstr
  (inp :: HST inp
inp :/ instr :: Instr inp out
instr ::: out :: HST out
out) -> HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ InstrCallStack -> Instr inp out -> Instr inp out
forall (a :: [T]) (b :: [T]).
InstrCallStack -> Instr a b -> Instr a b
WithLoc InstrCallStack
loc Instr inp out
instr Instr inp out -> HST out -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST out
out
  (inp :: HST inp
inp :/ AnyOutInstr instr :: 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
$ InstrCallStack -> Instr inp out -> Instr inp out
forall (a :: [T]) (b :: [T]).
InstrCallStack -> Instr a b -> Instr a b
WithLoc InstrCallStack
loc Instr inp out
forall (out :: [T]). Instr inp out
instr)

-- | Check whether given types are structurally equal and annotations converge.
matchTypes
  :: forall t1 t2.
      (Each '[KnownT] [t1, t2])
  => Notes t1 -> Notes t2 -> Either TCTypeError (t1 :~: t2, Notes t1)
matchTypes :: Notes t1 -> Notes t2 -> Either TCTypeError (t1 :~: t2, Notes t1)
matchTypes n1 :: Notes t1
n1 n2 :: Notes t2
n2 = do
  t1 :~: t2
Refl <- Each '[KnownT] '[t1, t2] => Either TCTypeError (t1 :~: t2)
forall (a :: T) (b :: T).
Each '[KnownT] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @t1 @t2
  Notes t1
nr <- Notes t1 -> Notes t1 -> Either AnnConvergeError (Notes t1)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes t1
n1 Notes t1
Notes t2
n2 Either AnnConvergeError (Notes t1)
-> (AnnConvergeError -> TCTypeError)
-> Either TCTypeError (Notes t1)
forall (p :: * -> * -> *) a c b.
Bifunctor p =>
p a c -> (a -> b) -> p b c
`onFirst` AnnConvergeError -> TCTypeError
AnnError
  return (t1 :~: t2
forall k (a :: k). a :~: a
Refl, Notes t1
nr)

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

-- | Generic implementation for MEMeration
memImpl
  :: forall c memKey rs inp m .
    ( MemOp c
    , KnownT (MemOpKey c)
    , inp ~ (memKey : c : rs)
    , MonadReader InstrCallStack m
    , MonadError TCError m
    )
  => Notes (MemOpKey c)
  -> HST inp
  -> VarAnn
  -> m (SomeInstr inp)
memImpl :: Notes (MemOpKey c) -> HST inp -> VarAnn -> m (SomeInstr inp)
memImpl cKeyNotes :: Notes (MemOpKey c)
cKeyNotes inputHST :: HST inp
inputHST@(hst0 :: (Notes x, Dict (WellTyped x), VarAnn)
hst0 ::& _ ::& hstTail :: HST xs
hstTail) varAnn :: VarAnn
varAnn =
  case Each '[KnownT] '[memKey, MemOpKey c] =>
Either TCTypeError (memKey :~: MemOpKey c)
forall (a :: T) (b :: T).
Each '[KnownT] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @memKey  @(MemOpKey c) of
    Right Refl -> do
      Notes x
_ <- ExpandedInstr
-> HST inp
-> Maybe TypeContext
-> Either AnnConvergeError (Notes x)
-> m (Notes x)
forall (m :: * -> *) (ts :: [T]) a.
(MonadReader InstrCallStack m, MonadError TCError m,
 Typeable ts) =>
ExpandedInstr
-> HST ts -> Maybe TypeContext -> Either AnnConvergeError a -> m a
onTypeCheckInstrAnnErr ExpandedInstr
uInstr HST inp
inputHST
        (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) (Notes x -> Notes x -> Either AnnConvergeError (Notes x)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes x
memKeyNotes Notes x
Notes (MemOpKey c)
cKeyNotes)
      pure $ HST inp
inputHST HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/
        Instr inp ('TBool : xs)
forall (c :: T) (c :: [T]).
MemOp c =>
Instr (MemOpKey c : c : c) ('TBool : c)
MEM Instr inp ('TBool : xs) -> HST ('TBool : xs) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Notes 'TBool
forall (t :: T). SingI t => Notes t
starNotes, Dict (WellTyped 'TBool)
forall (a :: Constraint). a => Dict a
Dict, VarAnn
varAnn) (Notes 'TBool, Dict (WellTyped 'TBool), VarAnn)
-> HST xs -> HST ('TBool : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
hstTail)
    Left m :: TCTypeError
m ->
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). Typeable ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) TCTypeError
m
  where
    (memKeyNotes :: Notes x
memKeyNotes, Dict, _) = (Notes x, Dict (WellTyped x), VarAnn)
hst0
    uInstr :: ExpandedInstr
uInstr = VarAnn -> ExpandedInstr
forall op. VarAnn -> InstrAbstract op
Un.MEM VarAnn
varAnn

getImpl
  :: forall c getKey rs inp m .
    ( GetOp c, KnownT (GetOpKey c)
    , WellTyped (GetOpVal c)
    , inp ~ (getKey : c : rs)
    , MonadReader InstrCallStack m
    , MonadError TCError m
    )
  => Notes (GetOpKey c)
  -> HST inp
  -> Notes (GetOpVal c)
  -> VarAnn
  -> m (SomeInstr inp)
getImpl :: Notes (GetOpKey c)
-> HST inp -> Notes (GetOpVal c) -> VarAnn -> m (SomeInstr inp)
getImpl notesKeyC :: Notes (GetOpKey c)
notesKeyC inputHST :: HST inp
inputHST@(hst0 :: (Notes x, Dict (WellTyped x), VarAnn)
hst0 ::& _ ::& hstTail :: HST xs
hstTail) valueNotes :: Notes (GetOpVal c)
valueNotes varAnn :: VarAnn
varAnn =
  case Each '[KnownT] '[getKey, GetOpKey c] =>
Either TCTypeError (getKey :~: GetOpKey c)
forall (a :: T) (b :: T).
Each '[KnownT] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @getKey @(GetOpKey c) of
    Right Refl -> do
      Notes x
_ <- ExpandedInstr
-> HST inp
-> Maybe TypeContext
-> Either AnnConvergeError (Notes x)
-> m (Notes x)
forall (m :: * -> *) (ts :: [T]) a.
(MonadReader InstrCallStack m, MonadError TCError m,
 Typeable ts) =>
ExpandedInstr
-> HST ts -> Maybe TypeContext -> Either AnnConvergeError a -> m a
onTypeCheckInstrAnnErr ExpandedInstr
uInstr HST inp
inputHST
        (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) (Notes x -> Notes x -> Either AnnConvergeError (Notes x)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes x
getKeyNotes Notes x
Notes (GetOpKey c)
notesKeyC)
      pure $ HST inp
inputHST HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/
        Instr inp ('TOption (GetOpVal c) : xs)
forall (c :: T) (c :: [T]).
(GetOp c, KnownT (GetOpVal c)) =>
Instr (GetOpKey c : c : c) ('TOption (GetOpVal c) : c)
GET Instr inp ('TOption (GetOpVal c) : xs)
-> HST ('TOption (GetOpVal c) : xs) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((TypeAnn -> Notes (GetOpVal c) -> Notes ('TOption (GetOpVal c))
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
forall a. Default a => a
def Notes (GetOpVal c)
valueNotes, Dict (WellTyped ('TOption (GetOpVal c)))
forall (a :: Constraint). a => Dict a
Dict, VarAnn
varAnn) (Notes ('TOption (GetOpVal c)),
 Dict (WellTyped ('TOption (GetOpVal c))), VarAnn)
-> HST xs -> HST ('TOption (GetOpVal c) : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
hstTail)
    Left m :: TCTypeError
m ->
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). Typeable ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) TCTypeError
m
  where
    (getKeyNotes :: Notes x
getKeyNotes, Dict, _) = (Notes x, Dict (WellTyped x), VarAnn)
hst0
    uInstr :: ExpandedInstr
uInstr = VarAnn -> ExpandedInstr
forall op. VarAnn -> InstrAbstract op
Un.GET VarAnn
varAnn

updImpl
  :: forall c updKey updParams rs inp m .
    ( UpdOp c
    , KnownT (UpdOpKey c), KnownT (UpdOpParams c)
    , inp ~ (updKey : updParams : c : rs)
    , MonadReader InstrCallStack m
    , MonadError TCError m
    )
  => Notes (UpdOpKey c)
  -> HST inp
  -> Notes (UpdOpParams c)
  -> VarAnn
  -> m (SomeInstr inp)
updImpl :: Notes (UpdOpKey c)
-> HST inp -> Notes (UpdOpParams c) -> VarAnn -> m (SomeInstr inp)
updImpl cKeyNotes :: Notes (UpdOpKey c)
cKeyNotes inputHST :: HST inp
inputHST@(hst0 :: (Notes x, Dict (WellTyped x), VarAnn)
hst0 ::& hst1 :: (Notes x, Dict (WellTyped x), VarAnn)
hst1 ::& cTuple :: (Notes x, Dict (WellTyped x), VarAnn)
cTuple ::& hstTail :: HST xs
hstTail) cValueNotes :: Notes (UpdOpParams c)
cValueNotes varAnn :: VarAnn
varAnn =
  case (Each '[KnownT] '[updKey, UpdOpKey c] =>
Either TCTypeError (updKey :~: UpdOpKey c)
forall (a :: T) (b :: T).
Each '[KnownT] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @updKey @(UpdOpKey c), Each '[KnownT] '[updParams, UpdOpParams c] =>
Either TCTypeError (updParams :~: UpdOpParams c)
forall (a :: T) (b :: T).
Each '[KnownT] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @updParams @(UpdOpParams c)) of
    (Right Refl, Right Refl) -> do
      Notes x
_ <- ExpandedInstr
-> HST inp
-> Maybe TypeContext
-> Either AnnConvergeError (Notes x)
-> m (Notes x)
forall (m :: * -> *) (ts :: [T]) a.
(MonadReader InstrCallStack m, MonadError TCError m,
 Typeable ts) =>
ExpandedInstr
-> HST ts -> Maybe TypeContext -> Either AnnConvergeError a -> m a
onTypeCheckInstrAnnErr ExpandedInstr
uInstr HST inp
inputHST
        (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) (Notes x -> Notes x -> Either AnnConvergeError (Notes x)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes x
updKeyNotes Notes x
Notes (UpdOpKey c)
cKeyNotes)
      Notes x
_ <- ExpandedInstr
-> HST inp
-> Maybe TypeContext
-> Either AnnConvergeError (Notes x)
-> m (Notes x)
forall (m :: * -> *) (ts :: [T]) a.
(MonadReader InstrCallStack m, MonadError TCError m,
 Typeable ts) =>
ExpandedInstr
-> HST ts -> Maybe TypeContext -> Either AnnConvergeError a -> m a
onTypeCheckInstrAnnErr ExpandedInstr
uInstr HST inp
inputHST
        (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerValueType) (Notes x -> Notes x -> Either AnnConvergeError (Notes x)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes x
updValueNotes Notes x
Notes (UpdOpParams c)
cValueNotes)
      pure $ HST inp
inputHST HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/
        Instr inp (c : xs)
forall (c :: T) (s :: [T]).
UpdOp c =>
Instr (UpdOpKey c : UpdOpParams c : c : s) (c : s)
UPDATE Instr inp (c : xs) -> HST (c : xs) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: (((Notes x, Dict (WellTyped x), VarAnn)
cTuple (Notes x, Dict (WellTyped x), VarAnn)
-> ((Notes x, Dict (WellTyped x), VarAnn)
    -> (Notes c, Dict (WellTyped c), VarAnn))
-> (Notes c, Dict (WellTyped c), VarAnn)
forall a b. a -> (a -> b) -> b
& (VarAnn -> Identity VarAnn)
-> (Notes x, Dict (WellTyped x), VarAnn)
-> Identity (Notes c, Dict (WellTyped c), VarAnn)
forall s t a b. Field3 s t a b => Lens s t a b
_3 ((VarAnn -> Identity VarAnn)
 -> (Notes x, Dict (WellTyped x), VarAnn)
 -> Identity (Notes c, Dict (WellTyped c), VarAnn))
-> VarAnn
-> (Notes x, Dict (WellTyped x), VarAnn)
-> (Notes c, Dict (WellTyped c), VarAnn)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ VarAnn
varAnn) (Notes c, Dict (WellTyped c), VarAnn) -> HST xs -> HST (c : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
hstTail)
    (Left m :: TCTypeError
m, _) ->
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). Typeable ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) TCTypeError
m
    (_, Left m :: TCTypeError
m) ->
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). Typeable ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerValueType) TCTypeError
m
  where
    (updKeyNotes :: Notes x
updKeyNotes, Dict, _) = (Notes x, Dict (WellTyped x), VarAnn)
hst0
    (updValueNotes :: Notes x
updValueNotes, Dict, _) = (Notes x, Dict (WellTyped x), VarAnn)
hst1
    uInstr :: ExpandedInstr
uInstr = VarAnn -> ExpandedInstr
forall op. VarAnn -> InstrAbstract op
Un.UPDATE VarAnn
varAnn

sizeImpl
  :: (SizeOp c, inp ~ (c ': rs), Monad m)
  => HST inp
  -> VarAnn
  -> m (SomeInstr inp)
sizeImpl :: HST inp -> VarAnn -> m (SomeInstr inp)
sizeImpl i :: HST inp
i@(_ ::& rs :: HST xs
rs) vn :: 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
:/ Instr (c : xs) ('TNat : xs)
forall (c :: T) (s :: [T]). SizeOp c => Instr (c : s) ('TNat : s)
SIZE Instr (c : xs) ('TNat : xs)
-> HST ('TNat : xs) -> SomeInstrOut (c : xs)
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Notes 'TNat
forall (t :: T). SingI t => Notes t
starNotes, Dict (WellTyped 'TNat)
forall (a :: Constraint). a => Dict a
Dict, VarAnn
vn) (Notes 'TNat, Dict (WellTyped 'TNat), VarAnn)
-> HST xs -> HST ('TNat : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs)

sliceImpl
  :: (SliceOp c, Typeable c, inp ~ ('TNat ': 'TNat ': c ': rs), Monad m)
  => HST inp
  -> Un.VarAnn
  -> m (SomeInstr inp)
sliceImpl :: HST inp -> VarAnn -> m (SomeInstr inp)
sliceImpl i :: HST inp
i@(_ ::& _ ::& (cn :: Notes x
cn, Dict, cvn :: VarAnn
cvn) ::& rs :: HST xs
rs) vn :: VarAnn
vn = do
  let vn' :: VarAnn
vn' = VarAnn
vn VarAnn -> VarAnn -> VarAnn
forall k (t :: k). Annotation t -> Annotation t -> Annotation t
`orAnn` VarAnn -> VarAnn -> VarAnn
deriveVN "slice" VarAnn
cvn
      rn :: Notes ('TOption x)
rn = TypeAnn -> Notes x -> Notes ('TOption x)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
forall a. Default a => a
def Notes 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
:/ Instr ('TNat : 'TNat : x : xs) ('TOption x : xs)
forall (s :: T) (s :: [T]).
(SliceOp s, KnownT s) =>
Instr ('TNat : 'TNat : s : s) ('TOption s : s)
SLICE Instr ('TNat : 'TNat : x : xs) ('TOption x : xs)
-> HST ('TOption x : xs) -> SomeInstrOut ('TNat : 'TNat : x : xs)
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Notes ('TOption x)
rn, Dict (WellTyped ('TOption x))
forall (a :: Constraint). a => Dict a
Dict, VarAnn
vn') (Notes ('TOption x), Dict (WellTyped ('TOption x)), VarAnn)
-> HST xs -> HST ('TOption x : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> 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' :: HST inp -> VarAnn -> m (SomeInstr inp)
concatImpl' i :: HST inp
i@((NTList _ n :: Notes t
n, Dict, _) ::& rs :: HST xs
rs) vn :: 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
:/ Instr ('TList t : xs) (t : xs)
forall (s :: T) (s :: [T]).
ConcatOp s =>
Instr ('TList s : s) (s : s)
CONCAT' Instr ('TList t : xs) (t : xs)
-> HST (t : xs) -> SomeInstrOut ('TList t : xs)
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Notes t
n, Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict, VarAnn
vn) (Notes t, Dict (WellTyped t), VarAnn) -> HST xs -> HST (t : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs)

concatImpl
  :: ( ConcatOp c, inp ~ (c ': c ': rs)
     , WellTyped c
     , MonadReader InstrCallStack m
     , MonadError TCError m
     )
  => HST inp
  -> Un.VarAnn
  -> m (SomeInstr inp)
concatImpl :: HST inp -> VarAnn -> m (SomeInstr inp)
concatImpl i :: HST inp
i@((cn1 :: Notes x
cn1, _, _) ::& (cn2 :: Notes x
cn2, _, _) ::& rs :: HST xs
rs) vn :: VarAnn
vn = do
  Notes x
cn <- ExpandedInstr
-> HST inp
-> Maybe TypeContext
-> Either AnnConvergeError (Notes x)
-> m (Notes x)
forall (m :: * -> *) (ts :: [T]) a.
(MonadReader InstrCallStack m, MonadError TCError m,
 Typeable ts) =>
ExpandedInstr
-> HST ts -> Maybe TypeContext -> Either AnnConvergeError a -> m a
onTypeCheckInstrAnnErr (VarAnn -> ExpandedInstr
forall op. VarAnn -> InstrAbstract op
Un.CONCAT VarAnn
vn) HST inp
i (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ConcatArgument) (Notes x -> Notes x -> Either AnnConvergeError (Notes x)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes x
cn1 Notes x
Notes x
cn2)
  pure $ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ Instr (x : x : xs) (x : xs)
forall (c :: T) (s :: [T]). ConcatOp c => Instr (c : c : s) (c : s)
CONCAT Instr (x : x : xs) (x : xs)
-> HST (x : xs) -> SomeInstrOut (x : x : xs)
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Notes x
cn, Dict (WellTyped x)
forall (a :: Constraint). a => Dict a
Dict, VarAnn
vn) (Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> 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.
     ( ArithOp aop n m
     , Typeable (ArithRes aop n m ': s)
     , WellTyped (ArithRes aop n m)
     , inp ~ (n ': m ': s)
     , MonadReader InstrCallStack t
     , MonadError TCError t
     )
  => Instr inp (ArithRes aop n m ': s)
  -> HST inp
  -> VarAnn
  -> Un.ExpandedInstr
  -> t (SomeInstr inp)
arithImpl :: Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl mkInstr :: Instr inp (ArithRes aop n m : s)
mkInstr i :: HST inp
i@((an :: Notes x
an, _, _) ::& (bn :: Notes x
bn, _, _) ::& rs :: HST xs
rs) vn :: VarAnn
vn uInstr :: ExpandedInstr
uInstr = do
  case Proxy aop
-> Notes x
-> Notes x
-> Either AnnConvergeError (Notes (ArithRes aop x x))
forall k (aop :: k) (n :: T) (m :: T) (proxy :: k -> *).
ArithOp aop n m =>
proxy aop
-> Notes n
-> Notes m
-> Either AnnConvergeError (Notes (ArithRes aop n m))
convergeArith (Proxy aop
forall k (t :: k). Proxy t
Proxy @aop) Notes x
an Notes x
bn of
    Right cn :: Notes (ArithRes aop x x)
cn ->
      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 (ArithRes aop n m : s)
Instr inp (ArithRes aop n m : xs)
mkInstr Instr inp (ArithRes aop n m : xs)
-> HST (ArithRes aop n m : xs) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Notes (ArithRes aop n m)
Notes (ArithRes aop x x)
cn, Dict (WellTyped (ArithRes aop n m))
forall (a :: Constraint). a => Dict a
Dict, VarAnn
vn) (Notes (ArithRes aop n m), Dict (WellTyped (ArithRes aop n m)),
 VarAnn)
-> HST xs -> HST (ArithRes aop n m : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs)
    Left err :: AnnConvergeError
err -> do
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> t (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). Typeable ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TCTypeError -> t (SomeInstr inp))
-> TCTypeError -> t (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ AnnConvergeError -> TCTypeError
AnnError AnnConvergeError
err

addImpl
  :: forall a b inp rs m.
     ( Typeable rs
     , Each '[KnownT] [a, b]
     , inp ~ (a ': b ': rs)
     , MonadReader InstrCallStack m
     , MonadError TCError m
     )
  => Sing a -> Sing b
  -> HST inp
  -> VarAnn
  -> Un.ExpandedInstr
  -> m (SomeInstr inp)
addImpl :: Sing a
-> Sing b
-> HST inp
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr inp)
addImpl t1 :: Sing a
t1 t2 :: Sing b
t2 = case (Sing a
SingT a
t1, Sing b
SingT b
t2) of
  (STInt, STInt) -> Instr ('TInt : 'TInt : rs) (ArithRes Add 'TInt 'TInt : rs)
-> HST ('TInt : 'TInt : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TInt : 'TInt : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add Instr ('TInt : 'TInt : rs) (ArithRes Add 'TInt 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Add n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  (STInt, STNat) -> Instr ('TInt : 'TNat : rs) (ArithRes Add 'TInt 'TNat : rs)
-> HST ('TInt : 'TNat : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TInt : 'TNat : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add Instr ('TInt : 'TNat : rs) (ArithRes Add 'TInt 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Add n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  (STNat, STInt) -> Instr ('TNat : 'TInt : rs) (ArithRes Add 'TNat 'TInt : rs)
-> HST ('TNat : 'TInt : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TNat : 'TInt : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add Instr ('TNat : 'TInt : rs) (ArithRes Add 'TNat 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Add n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  (STNat, STNat) -> Instr ('TNat : 'TNat : rs) (ArithRes Add 'TNat 'TNat : rs)
-> HST ('TNat : 'TNat : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TNat : 'TNat : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add Instr ('TNat : 'TNat : rs) (ArithRes Add 'TNat 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Add n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  (STInt, STTimestamp) -> Instr
  ('TInt : 'TTimestamp : rs) (ArithRes Add 'TInt 'TTimestamp : rs)
-> HST ('TInt : 'TTimestamp : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TInt : 'TTimestamp : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add Instr
  ('TInt : 'TTimestamp : rs) (ArithRes Add 'TInt 'TTimestamp : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Add n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  (STTimestamp, STInt) -> Instr
  ('TTimestamp : 'TInt : rs) (ArithRes Add 'TTimestamp 'TInt : rs)
-> HST ('TTimestamp : 'TInt : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TTimestamp : 'TInt : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add Instr
  ('TTimestamp : 'TInt : rs) (ArithRes Add 'TTimestamp 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Add n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  (STMutez, STMutez) -> Instr ('TMutez : 'TMutez : rs) (ArithRes Add 'TMutez 'TMutez : rs)
-> HST ('TMutez : 'TMutez : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TMutez : 'TMutez : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add Instr ('TMutez : 'TMutez : rs) (ArithRes Add 'TMutez 'TMutez : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Add n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  _ -> \i :: HST inp
i _ uInstr :: ExpandedInstr
uInstr -> ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). Typeable 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 ((SingKind T, SingI a) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @a) ((SingKind T, SingI b) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @b)

edivImpl
  :: forall a b inp rs m.
     ( Typeable rs
     , Each '[KnownT] [a, b]
     , inp ~ (a ': b ': rs)
     , MonadReader InstrCallStack m
     , MonadError TCError m
     )
  => Sing a -> Sing b
  -> HST inp
  -> VarAnn
  -> Un.ExpandedInstr
  -> m (SomeInstr inp)
edivImpl :: Sing a
-> Sing b
-> HST inp
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr inp)
edivImpl t1 :: Sing a
t1 t2 :: Sing b
t2 = case (Sing a
SingT a
t1, Sing b
SingT b
t2) of
  (STInt, STInt) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(EDivOp n m, WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
 inp ~ (n : m : s), MonadReader InstrCallStack t,
 MonadError TCError t) =>
HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
  (STInt, STNat) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(EDivOp n m, WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
 inp ~ (n : m : s), MonadReader InstrCallStack t,
 MonadError TCError t) =>
HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
  (STNat, STInt) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(EDivOp n m, WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
 inp ~ (n : m : s), MonadReader InstrCallStack t,
 MonadError TCError t) =>
HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
  (STNat, STNat) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(EDivOp n m, WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
 inp ~ (n : m : s), MonadReader InstrCallStack t,
 MonadError TCError t) =>
HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
  (STMutez, STMutez) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(EDivOp n m, WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
 inp ~ (n : m : s), MonadReader InstrCallStack t,
 MonadError TCError t) =>
HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
  (STMutez, STNat) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(EDivOp n m, WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
 inp ~ (n : m : s), MonadReader InstrCallStack t,
 MonadError TCError t) =>
HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
  _ -> \i :: HST inp
i _ uInstr :: ExpandedInstr
uInstr -> ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). Typeable 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 ((SingKind T, SingI a) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @a) ((SingKind T, SingI b) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @b)

edivImplDo
  :: ( EDivOp n m
     , WellTyped (EModOpRes n m)
     , WellTyped (EDivOpRes n m)
     , inp ~ (n ': m ': s)
     , MonadReader InstrCallStack t
     , MonadError TCError t
     )
  => HST inp
  -> VarAnn
  -> Un.ExpandedInstr
  -> t (SomeInstr inp)
edivImplDo :: HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo i :: HST inp
i@((an :: Notes x
an, _, _) ::& (bn :: Notes x
bn, _, _) ::& rs :: HST xs
rs) vn :: VarAnn
vn uInstr :: ExpandedInstr
uInstr = do
  case Notes x
-> Notes x
-> Either
     AnnConvergeError
     (Notes ('TOption ('TPair (EDivOpRes x x) (EModOpRes x x))))
forall (n :: T) (m :: T).
EDivOp n m =>
Notes n
-> Notes m
-> Either
     AnnConvergeError
     (Notes ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m))))
convergeEDiv Notes x
an Notes x
bn of
    Right cn :: Notes ('TOption ('TPair (EDivOpRes x x) (EModOpRes x x)))
cn ->
      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
  (n : m : s)
  ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : xs)
forall (n :: T) (m :: T) (s :: [T]).
EDivOp n m =>
Instr
  (n : m : s) ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : s)
EDIV 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]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Notes ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
Notes ('TOption ('TPair (EDivOpRes x x) (EModOpRes x x)))
cn, Dict
  (WellTyped ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m))))
forall (a :: Constraint). a => Dict a
Dict, VarAnn
vn) (Notes ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m))),
 Dict
   (WellTyped ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))),
 VarAnn)
-> HST xs
-> HST ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs)
    Left err :: AnnConvergeError
err -> do
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> t (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). Typeable ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TCTypeError -> t (SomeInstr inp))
-> TCTypeError -> t (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ AnnConvergeError -> TCTypeError
AnnError AnnConvergeError
err

subImpl
  :: forall a b inp rs m.
     ( Typeable rs
     , Each '[KnownT] [a, b]
     , inp ~ (a ': b ': rs)
     , MonadReader InstrCallStack m
     , MonadError TCError m
     )
  => Sing a -> Sing b
  -> HST inp
  -> VarAnn
  -> Un.ExpandedInstr
  -> m (SomeInstr inp)
subImpl :: Sing a
-> Sing b
-> HST inp
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr inp)
subImpl t1 :: Sing a
t1 t2 :: Sing b
t2 = case (Sing a
SingT a
t1, Sing b
SingT b
t2) of
  (STInt, STInt) -> Instr ('TInt : 'TInt : rs) (ArithRes Sub 'TInt 'TInt : rs)
-> HST ('TInt : 'TInt : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TInt : 'TInt : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Sub Instr ('TInt : 'TInt : rs) (ArithRes Sub 'TInt 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Sub n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Sub n m : s)
SUB
  (STInt, STNat) -> Instr ('TInt : 'TNat : rs) (ArithRes Sub 'TInt 'TNat : rs)
-> HST ('TInt : 'TNat : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TInt : 'TNat : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Sub Instr ('TInt : 'TNat : rs) (ArithRes Sub 'TInt 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Sub n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Sub n m : s)
SUB
  (STNat, STInt) -> Instr ('TNat : 'TInt : rs) (ArithRes Sub 'TNat 'TInt : rs)
-> HST ('TNat : 'TInt : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TNat : 'TInt : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Sub Instr ('TNat : 'TInt : rs) (ArithRes Sub 'TNat 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Sub n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Sub n m : s)
SUB
  (STNat, STNat) -> Instr ('TNat : 'TNat : rs) (ArithRes Sub 'TNat 'TNat : rs)
-> HST ('TNat : 'TNat : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TNat : 'TNat : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Sub Instr ('TNat : 'TNat : rs) (ArithRes Sub 'TNat 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Sub n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Sub n m : s)
SUB
  (STTimestamp, STTimestamp) -> Instr
  ('TTimestamp : 'TTimestamp : rs)
  (ArithRes Sub 'TTimestamp 'TTimestamp : rs)
-> HST ('TTimestamp : 'TTimestamp : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TTimestamp : 'TTimestamp : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Sub Instr
  ('TTimestamp : 'TTimestamp : rs)
  (ArithRes Sub 'TTimestamp 'TTimestamp : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Sub n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Sub n m : s)
SUB
  (STTimestamp, STInt) -> Instr
  ('TTimestamp : 'TInt : rs) (ArithRes Sub 'TTimestamp 'TInt : rs)
-> HST ('TTimestamp : 'TInt : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TTimestamp : 'TInt : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Sub Instr
  ('TTimestamp : 'TInt : rs) (ArithRes Sub 'TTimestamp 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Sub n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Sub n m : s)
SUB
  (STMutez, STMutez) -> Instr ('TMutez : 'TMutez : rs) (ArithRes Sub 'TMutez 'TMutez : rs)
-> HST ('TMutez : 'TMutez : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TMutez : 'TMutez : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Sub Instr ('TMutez : 'TMutez : rs) (ArithRes Sub 'TMutez 'TMutez : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Sub n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Sub n m : s)
SUB
  _ -> \i :: HST inp
i _ uInstr :: ExpandedInstr
uInstr -> ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). Typeable 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 ((SingKind T, SingI a) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @a) ((SingKind T, SingI b) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @b)

mulImpl
  :: forall a b inp rs m.
     ( Typeable rs
     , Each '[KnownT] [a, b]
     , inp ~ (a ': b ': rs)
     , MonadReader InstrCallStack m
     , MonadError TCError m
     )
  => Sing a -> Sing b
  -> HST inp
  -> VarAnn
  -> Un.ExpandedInstr
  -> m (SomeInstr inp)
mulImpl :: Sing a
-> Sing b
-> HST inp
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr inp)
mulImpl t1 :: Sing a
t1 t2 :: Sing b
t2 = case (Sing a
SingT a
t1, Sing b
SingT b
t2) of
  (STInt, STInt) -> Instr ('TInt : 'TInt : rs) (ArithRes Mul 'TInt 'TInt : rs)
-> HST ('TInt : 'TInt : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TInt : 'TInt : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul Instr ('TInt : 'TInt : rs) (ArithRes Mul 'TInt 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Mul n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (STInt, STNat) -> Instr ('TInt : 'TNat : rs) (ArithRes Mul 'TInt 'TNat : rs)
-> HST ('TInt : 'TNat : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TInt : 'TNat : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul Instr ('TInt : 'TNat : rs) (ArithRes Mul 'TInt 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Mul n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (STNat, STInt) -> Instr ('TNat : 'TInt : rs) (ArithRes Mul 'TNat 'TInt : rs)
-> HST ('TNat : 'TInt : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TNat : 'TInt : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul Instr ('TNat : 'TInt : rs) (ArithRes Mul 'TNat 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Mul n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (STNat, STNat) -> Instr ('TNat : 'TNat : rs) (ArithRes Mul 'TNat 'TNat : rs)
-> HST ('TNat : 'TNat : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TNat : 'TNat : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul Instr ('TNat : 'TNat : rs) (ArithRes Mul 'TNat 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Mul n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (STNat, STMutez) -> Instr ('TNat : 'TMutez : rs) (ArithRes Mul 'TNat 'TMutez : rs)
-> HST ('TNat : 'TMutez : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TNat : 'TMutez : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul Instr ('TNat : 'TMutez : rs) (ArithRes Mul 'TNat 'TMutez : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Mul n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (STMutez, STNat) -> Instr ('TMutez : 'TNat : rs) (ArithRes Mul 'TMutez 'TNat : rs)
-> HST ('TMutez : 'TNat : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TMutez : 'TNat : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, Typeable (ArithRes aop n m : s),
 WellTyped (ArithRes aop n m), inp ~ (n : m : s),
 MonadReader InstrCallStack t, MonadError TCError t) =>
Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul Instr ('TMutez : 'TNat : rs) (ArithRes Mul 'TMutez 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
(ArithOp Mul n m, Typeable n, Typeable m) =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  _ -> \i :: HST inp
i _ uInstr :: ExpandedInstr
uInstr -> ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). Typeable 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 ((SingKind T, SingI a) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @a) ((SingKind T, SingI b) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @b)

-- | Helper function to construct instructions for unary arithmetic
-- operations.
unaryArithImpl
  :: ( Typeable (UnaryArithRes aop n ': s)
     , WellTyped (UnaryArithRes aop n)
     , inp ~ (n ': s)
     , Monad t
     )
  => Instr inp (UnaryArithRes aop n ': s)
  -> HST inp
  -> VarAnn
  -> t (SomeInstr inp)
unaryArithImpl :: Instr inp (UnaryArithRes aop n : s)
-> HST inp -> VarAnn -> t (SomeInstr inp)
unaryArithImpl mkInstr :: Instr inp (UnaryArithRes aop n : s)
mkInstr i :: HST inp
i@(_ ::& rs :: HST xs
rs) vn :: VarAnn
vn = 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]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Notes (UnaryArithRes aop n)
forall (t :: T). SingI t => Notes t
starNotes, Dict (WellTyped (UnaryArithRes aop n))
forall (a :: Constraint). a => Dict a
Dict, VarAnn
vn) (Notes (UnaryArithRes aop n),
 Dict (WellTyped (UnaryArithRes aop n)), VarAnn)
-> HST xs -> HST (UnaryArithRes aop n : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs)

-- | Helper function to construct instructions for unary arithmetic
-- operations that should preserve annotations.
unaryArithImplAnnotated
  :: ( Typeable (UnaryArithRes aop n ': s)
     , WellTyped (UnaryArithRes aop n)
     , inp ~ (n ': s)
     , Monad t
     , n ~ UnaryArithRes aop n
     )
  => Instr inp (UnaryArithRes aop n ': s)
  -> HST inp
  -> VarAnn
  -> t (SomeInstr inp)
unaryArithImplAnnotated :: Instr inp (UnaryArithRes aop n : s)
-> HST inp -> VarAnn -> t (SomeInstr inp)
unaryArithImplAnnotated mkInstr :: Instr inp (UnaryArithRes aop n : s)
mkInstr i :: HST inp
i@((n :: Notes x
n, _, _) ::& rs :: HST xs
rs) vn :: VarAnn
vn = 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]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Notes x
n, Dict (WellTyped x)
forall (a :: Constraint). a => Dict a
Dict, VarAnn
vn) (Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs)