-- 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
    , getUpdImpl
    , sliceImpl
    , concatImpl
    , concatImpl'
    , sizeImpl
    , arithImpl
    , addImpl
    , subImpl
    , mulImpl
    , edivImpl
    , unaryArithImpl
    , unaryArithImplAnnotated
    , withCompareableCheck
    ) where

import Prelude hiding (EQ, GT, LT)

import Control.Lens (unsnoc)
import Control.Monad.Except (MonadError, throwError)
import Data.Constraint (Dict(..), withDict)
import Data.Default (def)
import Data.Singletons (Sing, SingI(sing), demote)
import Data.Singletons.Decide
import qualified Data.Text as T
import Data.Vinyl (Rec(..))
import Fmt ((+||), (||+))

import Michelson.ErrorPos (InstrCallStack)
import Michelson.TypeCheck.Error (TCError(..), TCTypeError(..), TypeContext(..))
import Michelson.TypeCheck.TypeCheck
import Michelson.TypeCheck.TypeCheckedSeq (IllTypedInstr(..), TypeCheckedSeq(..))
import Michelson.TypeCheck.Types
import Michelson.Typed
  (BadTypeForScope(..), CommentType(StackTypeComment), Comparable, ExtInstr(COMMENT_ITEM),
  Instr(..), Notes(..), SingT(..), T(..), WellTyped, converge, getComparableProofS, notesT,
  requireEq, 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, annQ, noAnn, orAnn, unsafeMkAnnotation)
import Util.Sing (eqI)
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
  -> (VarAnn, FieldAnn, FieldAnn)
deriveSpecialFNs :: FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> VarAnn
-> (VarAnn, FieldAnn, FieldAnn)
deriveSpecialFNs FieldAnn
pfn FieldAnn
qfn VarAnn
pvn VarAnn
qvn VarAnn
vn = (VarAnn
vn', FieldAnn
pfn', FieldAnn
qfn')
  where
    (VarAnn
vn1, FieldAnn
pfn') = (VarAnn, FieldAnn)
-> (VarAnn, FieldAnn) -> Bool -> (VarAnn, FieldAnn)
forall a. a -> a -> Bool -> a
bool (VarAnn
vn, FieldAnn
pfn) (VarAnn -> (VarAnn, FieldAnn)
splitLastDot VarAnn
pvn) (FieldAnn -> Text
forall k (tag :: k). Annotation tag -> Text
unAnnotation FieldAnn
pfn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"@")
    (VarAnn
vn2, FieldAnn
qfn') = (VarAnn, FieldAnn)
-> (VarAnn, FieldAnn) -> Bool -> (VarAnn, FieldAnn)
forall a. a -> a -> Bool -> a
bool (VarAnn
vn, FieldAnn
qfn) (VarAnn -> (VarAnn, FieldAnn)
splitLastDot VarAnn
qvn) (FieldAnn -> Text
forall k (tag :: k). Annotation tag -> Text
unAnnotation FieldAnn
qfn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"@")
    vn' :: VarAnn
vn' = VarAnn -> VarAnn -> Bool -> VarAnn
forall a. a -> a -> Bool -> a
bool VarAnn
vn (VarAnn -> VarAnn -> VarAnn
commonPrefix VarAnn
vn1 VarAnn
vn2) (VarAnn
vn VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
forall a. Default a => a
def)

    splitLastDot :: VarAnn -> (VarAnn, FieldAnn)
    splitLastDot :: VarAnn -> (VarAnn, FieldAnn)
splitLastDot VarAnn
v = case [Text] -> Maybe ([Text], Text)
forall s a. Snoc s s a a => s -> Maybe (s, a)
unsnoc ([Text] -> Maybe ([Text], Text)) -> [Text] -> Maybe ([Text], Text)
forall a b. (a -> b) -> a -> b
$ Text -> Text -> [Text]
T.splitOn Text
"." (Text -> [Text]) -> Text -> [Text]
forall a b. (a -> b) -> a -> b
$ VarAnn -> Text
forall k (tag :: k). Annotation tag -> Text
unAnnotation VarAnn
v of
      Maybe ([Text], Text)
Nothing      -> (VarAnn, FieldAnn)
forall a. Default a => a
def
      Just ([Text]
_, Text
"") -> (VarAnn
forall a. Default a => a
def, VarAnn -> FieldAnn
forall k1 k2 (tag1 :: k1) (tag2 :: k2).
Annotation tag1 -> Annotation tag2
Un.convAnn VarAnn
v)
      Just ([Text]
vs, Text
l) -> ((Element [Text] -> VarAnn) -> [Text] -> VarAnn
forall t m. (Container t, Monoid m) => (Element t -> m) -> t -> m
foldMap Element [Text] -> VarAnn
forall k (a :: k). HasCallStack => Text -> Annotation a
unsafeMkAnnotation [Text]
vs, FieldAnn -> FieldAnn -> Bool -> FieldAnn
forall a. a -> a -> Bool -> a
bool (Text -> FieldAnn
forall k (a :: k). HasCallStack => Text -> Annotation a
unsafeMkAnnotation Text
l) FieldAnn
forall a. Default a => a
def (Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"car" Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
|| Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"cdr"))

    commonPrefix :: VarAnn -> VarAnn -> VarAnn
    commonPrefix :: VarAnn -> VarAnn -> VarAnn
commonPrefix = ((VarAnn, VarAnn) -> VarAnn) -> VarAnn -> VarAnn -> VarAnn
forall a b c. ((a, b) -> c) -> a -> b -> c
curry \case
      (VarAnn
v1, VarAnn
v2) | VarAnn
v1 VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
v2 -> VarAnn
v1
      (VarAnn
v1, VarAnn
v2) | VarAnn
v2 VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
forall k (a :: k). Annotation a
noAnn -> VarAnn
v1
      (VarAnn
v1, VarAnn
v2) | VarAnn
v1 VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
forall k (a :: k). Annotation a
noAnn -> VarAnn
v2
      (VarAnn, VarAnn)
_ -> VarAnn
forall a. Default a => a
def

-- | Function which derives special annotations
-- for CDR / CAR instructions.
deriveSpecialVN :: VarAnn -> FieldAnn -> VarAnn -> VarAnn -> VarAnn
deriveSpecialVN :: VarAnn -> FieldAnn -> VarAnn -> VarAnn -> VarAnn
deriveSpecialVN VarAnn
vn FieldAnn
elFn VarAnn
pairVN VarAnn
elVn
  | (VarAnn -> Text
forall k (tag :: k). Annotation tag -> Text
unAnnotation VarAnn
vn) Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"%" = FieldAnn -> VarAnn
forall k1 k2 (tag1 :: k1) (tag2 :: k2).
Annotation tag1 -> Annotation tag2
Un.convAnn FieldAnn
elFn
  -- TODO [#534]:
  -- In the `%%` branch, if the pair's field annotation (`elFn`) is empty, we should default it to "cdr"/"car".
  -- See: <https://tezos.gitlab.io/008/michelson.html#automatic-variable-and-field-annotations-inferring>
  | (VarAnn -> Text
forall k (tag :: k). Annotation tag -> Text
unAnnotation VarAnn
vn) Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"%%" = 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 VarAnn -> VarAnn -> VarAnn
forall k (t :: k). Annotation t -> Annotation t -> Annotation t
`orAnn` VarAnn
elVn

-- | Append suffix to variable annotation (if it's not empty)
deriveVN :: VarAnn -> VarAnn -> VarAnn
deriveVN :: VarAnn -> VarAnn -> VarAnn
deriveVN VarAnn
suffix 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 TypeAnn
_ FieldAnn
afn FieldAnn
bfn Notes p
an Notes q
bn) 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` [annQ|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` [annQ|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 TypeAnn
_ Notes t
an) VarAnn
ovn =
  let avn :: VarAnn
avn = VarAnn -> VarAnn -> VarAnn
deriveVN [annQ|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 (Notes t
an, d :: Dict (WellTyped t)
d@Dict (WellTyped t)
Dict, VarAnn
avn) (Notes t
bn, Dict (WellTyped t)
_, 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 HST ts
SNil HST ts
SNil = HST '[] -> Either AnnConvergeError (HST '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure HST '[]
SNil
convergeHST ((Notes x, Dict (WellTyped x), VarAnn)
a ::& HST xs
as) ((Notes x, Dict (WellTyped x), VarAnn)
b ::& 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 (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(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
  HST st
SNil -> []
  (Notes x
notes, Dict (WellTyped x)
_, VarAnn
_) ::& 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. (SingI as, SingI 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 (SingI as, SingI bs, TestEquality Sing) => Maybe (as :~: bs)
forall k (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @as @bs of
    Maybe (as :~: bs)
Nothing -> TCTypeError -> Either TCTypeError (as :~: bs)
forall a b. a -> Either a b
Left (TCTypeError -> Either TCTypeError (as :~: bs))
-> TCTypeError -> Either TCTypeError (as :~: bs)
forall a b. (a -> b) -> a -> b
$ [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 as :~: bs
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. (SingI st, WellTyped t)
  => HST st -> Either TCTypeError (st :~: '[t])
eqHST1 :: HST st -> Either TCTypeError (st :~: '[t])
eqHST1 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 (x :: T) (xs :: [T]).
(WellTyped x, SingI xs) =>
Sing x -> HST xs -> HST (x : xs)
-:& HST '[]
SNil
  case (SingI '[t], SingI st, TestEquality Sing) => Maybe ('[t] :~: st)
forall k (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @'[t] @st of
    Maybe ('[t] :~: st)
Nothing -> TCTypeError -> Either TCTypeError (st :~: '[t])
forall a b. a -> Either a b
Left (TCTypeError -> Either TCTypeError (st :~: '[t]))
-> TCTypeError -> Either TCTypeError (st :~: '[t])
forall a b. (a -> b) -> a -> b
$ [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 '[t] :~: st
Refl -> (st :~: st) -> Either TCTypeError (st :~: st)
forall a b. b -> Either a b
Right st :~: st
forall k (a :: k). a :~: a
Refl

lengthHST :: HST xs -> Natural
lengthHST :: HST xs -> Natural
lengthHST ((Notes x, Dict (WellTyped x), VarAnn)
_ ::& HST xs
xs) = Natural
1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ HST xs -> Natural
forall (xs :: [T]). HST xs -> Natural
lengthHST HST xs
xs
lengthHST HST xs
SNil = Natural
0

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

-- | Check whether elements go in strictly ascending order and
-- return the original list (to keep only one pass on the original list).
ensureDistinctAsc :: (Ord b, Show a) => (a -> b) -> [a] -> Either Text [a]
ensureDistinctAsc :: (a -> b) -> [a] -> Either Text [a]
ensureDistinctAsc a -> b
toCmp = \case
  (a
e1 : a
e2 : [a]
l) ->
    if a -> b
toCmp a
e1 b -> b -> Bool
forall a. Ord a => a -> a -> Bool
< a -> b
toCmp a
e2
    then (a
e1 a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> [a]) -> Either Text [a] -> Either Text [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> b) -> [a] -> Either Text [a]
forall b a. (Ord b, 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
$ Builder
"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 -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+|| a
e2 a -> Builder -> Builder
forall a b. (Show a, FromBuilder b) => a -> Builder -> b
||+ Builder
")"
  [a]
l -> [a] -> Either Text [a]
forall a b. b -> Either a b
Right [a]
l

-- | Function @eqType@ is a simple wrapper around @Data.Singletons.decideEquality@ suited
-- for use within @Either TCTypeError a@ applicative.
eqType
  :: forall (a :: T) (b :: T). (Each '[SingI] [a, b])
  => Either TCTypeError (a :~: b)
eqType :: Either TCTypeError (a :~: b)
eqType =
  forall (a :: T) (b :: T) (m :: * -> *).
(SingI a, SingI b, Monad m) =>
(forall x. Demote T -> Demote T -> m x) -> m (a :~: b)
forall (m :: * -> *).
(SingI a, SingI b, Monad m) =>
(forall x. Demote T -> Demote T -> m x) -> m (a :~: b)
requireEq @a @b ((forall x. Demote T -> Demote T -> Either TCTypeError x)
 -> Either TCTypeError (a :~: b))
-> (forall x. Demote T -> Demote T -> Either TCTypeError x)
-> Either TCTypeError (a :~: b)
forall a b. (a -> b) -> a -> b
$ TCTypeError -> Either TCTypeError x
forall a b. a -> Either a b
Left (TCTypeError -> Either TCTypeError x)
-> (T -> T -> TCTypeError) -> T -> T -> Either TCTypeError x
forall a b c. SuperComposition a b c => a -> b -> c
... T -> T -> TCTypeError
TypeEqError

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 ExpandedInstr
instr SomeHST
hst Maybe TypeContext
mContext Either TCTypeError a
ei = do
  (TCTypeError -> m a) -> (a -> m a) -> Either TCTypeError a -> m a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
forall (m :: * -> *) a.
(MonadReader 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 ExpandedInstr
instr SomeHST
hst Maybe TypeContext
mContext = \case
  Right a
a -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
  Left BadTypeForScope
e -> do
    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 ExpandedInstr
instr SomeHST
hst 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' ExpandedInstr
instr SomeHST
hst Maybe TypeContext
mContext 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, SingI ts)
  => Un.ExpandedInstr -> HST ts -> Maybe TypeContext
  -> Either AnnConvergeError a -> m a
onTypeCheckInstrAnnErr :: ExpandedInstr
-> HST ts -> Maybe TypeContext -> Either AnnConvergeError a -> m a
onTypeCheckInstrAnnErr ExpandedInstr
instr HST ts
i Maybe TypeContext
mContext 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]). SingI 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. (SingI 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 Sing a
sng ExpandedInstr
instr HST ts
i Comparable a => v
act = case Sing a -> Maybe (Dict (Comparable a))
forall (a :: T). Sing a -> Maybe (Dict (Comparable a))
getComparableProofS Sing a
sng of
  Just d :: Dict (Comparable a)
d@Dict (Comparable a)
Dict -> v -> m v
forall (f :: * -> *) a. Applicative f => a -> f a
pure (v -> m v) -> v -> m v
forall a b. (a -> b) -> a -> b
$ Dict (Comparable a) -> (Comparable a => v) -> v
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict Dict (Comparable a)
d Comparable a => v
act
  Maybe (Dict (Comparable a))
Nothing -> ExpandedInstr -> SomeHST -> Maybe TypeContext -> m v
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> m a
typeCheckInstrErr ExpandedInstr
instr (HST ts -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST ts
i) (Maybe TypeContext -> m v) -> Maybe TypeContext -> m v
forall a b. (a -> b) -> a -> b
$ TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ComparisonArguments

typeCheckOpImpl
  :: forall inp. SingI inp
  => TcInstrHandler
  -> Un.ExpandedOp
  -> HST inp
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl :: TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op' HST inp
hst = case ExpandedOp
op' of
  Un.WithSrcEx InstrCallStack
_ op :: ExpandedOp
op@Un.WithSrcEx{} -> TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op HST inp
hst
  Un.WithSrcEx InstrCallStack
loc (Un.PrimEx ExpandedInstr
op)  -> InstrCallStack
-> ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrimWithLoc InstrCallStack
loc ExpandedInstr
op
  Un.WithSrcEx InstrCallStack
loc (Un.SeqEx [ExpandedOp]
sq)   -> InstrCallStack
-> [ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeqWithLoc InstrCallStack
loc [ExpandedOp]
sq
  Un.PrimEx ExpandedInstr
op                     -> ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrim ExpandedInstr
op
  Un.SeqEx [ExpandedOp]
sq                      -> [ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeq [ExpandedOp]
sq
  where
    -- If we know source location from the untyped instruction, keep it in the typed one.
    typeCheckPrimWithLoc :: InstrCallStack -> Un.ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
    typeCheckPrimWithLoc :: InstrCallStack
-> ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrimWithLoc InstrCallStack
loc 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 ExpandedInstr
op = ExpandedInstr
-> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
TcInstrHandler
tcInstr ExpandedInstr
op HST inp
hst 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 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 [ExpandedOp]
sq = TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl TcInstrHandler
tcInstr [ExpandedOp]
sq HST inp
hst
                  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 (HST inp
inp :/ Instr inp out
i ::: HST out
out) = HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ 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]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST out
out
    addNotes 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 HST d
outputStack Instr c d
instr = case Instr c d
instr of
      -- Abstractions for instructions:
      Instr c d
Nop -> Instr c d
instr'
      Seq Instr c b
_ Instr b d
_ -> Instr c d
instr'
      Nested Instr c d
_ -> Instr c d
instr'
      DocGroup DocGrouping
_ Instr c d
_ -> Instr c d
instr'
      Ext ExtInstr c
_ -> Instr c d
instr'
      FrameInstr Proxy s
_ Instr a b
_ -> Instr c d
instr'
      WithLoc InstrCallStack
_ Instr c d
_ -> Instr c d
instr'
      Fn {} -> Instr c d
instr'
      -- These three shouldn't happen, since annotations are added here.
      InstrWithNotes {} -> Instr c d
instr'
      InstrWithVarAnns VarAnns
_ Instr c d
_ -> Instr c d
instr'
      InstrWithVarNotes NonEmpty VarAnn
_ Instr c d
_ -> Instr c d
instr'

      -- Instructions that don't produce notes:
      Instr c d
DROP -> Instr c d
instr'
      DROPN PeanoNatural n
_ -> Instr c d
instr'
      Instr c d
SWAP -> Instr c d
instr'
      DIG PeanoNatural n
_ -> Instr c d
instr'
      DUG PeanoNatural n
_ -> Instr c d
instr'
      IF_NONE Instr s d
_ Instr (a : s) d
_ -> Instr c d
instr'
      IF_LEFT Instr (a : s) d
_ Instr (b : s) d
_ -> Instr c d
instr'
      IF_CONS Instr (a : 'TList a : s) d
_ Instr s d
_ -> Instr c d
instr'
      ITER Instr (IterOpEl c : d) d
_ -> Instr c d
instr'
      IF Instr s d
_ Instr s d
_ -> Instr c d
instr'
      LOOP Instr d ('TBool : d)
_ -> Instr c d
instr'
      LOOP_LEFT Instr (a : s) ('TOr a b : s)
_ -> Instr c d
instr'
      DIP Instr a c
_ -> Instr c d
instr'
      DIPN PeanoNatural n
_ Instr s s'
_ -> Instr c d
instr'
      Instr c d
FAILWITH -> Instr c d
instr'
      Instr c d
NEVER -> Instr c d
instr'

      -- These instructions technically may have one/two explicit var anns, BUT because they support special var anns,
      -- the var anns are stored directly inside the instruction's constructor.
      -- For this reason, they must NOT be wrapped in `InstrWithVarNotes`.
      AnnCAR VarAnn
_ FieldAnn
_ -> Instr c d
instr'
      AnnCDR VarAnn
_ FieldAnn
_ -> Instr c d
instr'
      AnnUNPAIR{} ->
        case HST d
outputStack of
          (Notes x
notes1, Dict (WellTyped x)
_, VarAnn
varAnn1) ::& (Notes x
notes2, Dict (WellTyped x)
_, VarAnn
varAnn2) ::& HST xs
_ ->
            let withNotes :: Instr c d -> Instr c d
withNotes
                  | Notes x -> Bool
forall (t :: T). SingI t => Notes t -> Bool
isStar Notes x
notes1 Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
&& Notes x -> Bool
forall (t :: T). SingI t => Notes t -> Bool
isStar Notes x
notes2 = Instr c d -> Instr c d
forall a. a -> a
id
                  | Notes x -> Bool
forall (t :: T). SingI t => Notes t -> Bool
isStar Notes x
notes2 = Proxy (b : s)
-> Rec Notes '[x]
-> Instr ('TPair a b : s) ('[x] ++ (b : s))
-> Instr ('TPair a b : s) ('[x] ++ (b : s))
forall (a :: [T]) (topElems :: [T]) (s :: [T]).
(RMap topElems, RecordToList topElems,
 ReifyConstraint Show Notes topElems,
 ReifyConstraint NFData Notes topElems, Each '[SingI] topElems) =>
Proxy s
-> Rec Notes topElems
-> Instr a (topElems ++ s)
-> Instr a (topElems ++ s)
InstrWithNotes Proxy (b : s)
forall k (t :: k). Proxy t
Proxy (Notes x
notes1 Notes x -> Rec Notes '[] -> Rec Notes '[x]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Notes '[]
forall u (a :: u -> *). Rec a '[]
RNil)
                  | Bool
otherwise = Proxy s
-> Rec Notes '[x, x]
-> Instr ('TPair a b : s) ('[x, x] ++ s)
-> Instr ('TPair a b : s) ('[x, x] ++ s)
forall (a :: [T]) (topElems :: [T]) (s :: [T]).
(RMap topElems, RecordToList topElems,
 ReifyConstraint Show Notes topElems,
 ReifyConstraint NFData Notes topElems, Each '[SingI] topElems) =>
Proxy s
-> Rec Notes topElems
-> Instr a (topElems ++ s)
-> Instr a (topElems ++ s)
InstrWithNotes Proxy s
forall k (t :: k). Proxy t
Proxy (Notes x
notes1 Notes x -> Rec Notes '[x] -> Rec Notes '[x, x]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Notes x
notes2 Notes x -> Rec Notes '[] -> Rec Notes '[x]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Notes '[]
forall u (a :: u -> *). Rec a '[]
RNil)
                withVarAnns :: Instr c d -> Instr c d
withVarAnns
                  | VarAnn
varAnn1 VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
forall a. Default a => a
def Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
&& VarAnn
varAnn2 VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
forall a. Default a => a
def = Instr c d -> Instr c d
forall a. a -> a
id
                  | VarAnn
varAnn2 VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
forall a. Default a => a
def = VarAnns -> Instr c d -> Instr c d
forall (a :: [T]) (b :: [T]). VarAnns -> Instr a b -> Instr a b
InstrWithVarAnns (VarAnns -> Instr c d -> Instr c d)
-> VarAnns -> Instr c d -> Instr c d
forall a b. (a -> b) -> a -> b
$ VarAnn -> VarAnns
Un.OneVarAnn VarAnn
varAnn1
                  | Bool
otherwise = VarAnns -> Instr c d -> Instr c d
forall (a :: [T]) (b :: [T]). VarAnns -> Instr a b -> Instr a b
InstrWithVarAnns (VarAnn -> VarAnn -> VarAnns
Un.TwoVarAnns VarAnn
varAnn1 VarAnn
varAnn2)
            in Instr c d -> Instr c d
withNotes (Instr c d -> Instr c d) -> Instr c d -> Instr c d
forall a b. (a -> b) -> a -> b
$ Instr c d -> Instr c d
withVarAnns Instr c d
instr

      -- We purposefully don't wrap `UNPAIRN` in meta-instructions
      -- like `InstrWithNotes` and `InstrWithVarAnns`.
      -- See !769 for a lengthy explanation.
      UNPAIRN PeanoNatural n
_ -> Instr c d
instr

      -- Instructions that produce at most two notes:
      CREATE_CONTRACT Contract p g
_ -> case HST d
outputStack of
        ((Notes x
np, Dict (WellTyped x)
_, VarAnn
vp) ::& (Notes x
_, Dict (WellTyped x)
_, VarAnn
vs) ::& HST xs
_) ->
          let withNotes :: Instr c d -> Instr c d
withNotes = if Notes x -> Bool
forall (t :: T). SingI t => Notes t -> Bool
isStar Notes x
np then Instr c d -> Instr c d
forall a. a -> a
id else Proxy ('TAddress : s)
-> Rec Notes '[x]
-> Instr
     ('TOption 'TKeyHash : 'TMutez : g : s) ('[x] ++ ('TAddress : s))
-> Instr
     ('TOption 'TKeyHash : 'TMutez : g : s) ('[x] ++ ('TAddress : s))
forall (a :: [T]) (topElems :: [T]) (s :: [T]).
(RMap topElems, RecordToList topElems,
 ReifyConstraint Show Notes topElems,
 ReifyConstraint NFData Notes topElems, Each '[SingI] topElems) =>
Proxy s
-> Rec Notes topElems
-> Instr a (topElems ++ s)
-> Instr a (topElems ++ s)
InstrWithNotes Proxy ('TAddress : s)
forall k (t :: k). Proxy t
Proxy (Notes x
np Notes x -> Rec Notes '[] -> Rec Notes '[x]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Notes '[]
forall u (a :: u -> *). Rec a '[]
RNil)
              withVarNotes :: Instr c d -> Instr c d
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
forall a. Boolean a => a -> a -> a
&& VarAnn
vs VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
forall k (a :: k). Annotation a
Un.noAnn then Instr c d -> Instr c d
forall a. a -> a
id else NonEmpty VarAnn -> Instr c d -> Instr c d
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])
              withVarNotes' :: Instr c d -> Instr c d
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
forall a. Boolean a => a -> a -> a
&& VarAnn
vs VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
forall k (a :: k). Annotation a
Un.noAnn then Instr c d -> Instr c d
forall a. a -> a
id else VarAnns -> Instr c d -> Instr c d
forall (a :: [T]) (b :: [T]). VarAnns -> Instr a b -> Instr a b
InstrWithVarAnns (VarAnns -> Instr c d -> Instr c d)
-> VarAnns -> Instr c d -> Instr c d
forall a b. (a -> b) -> a -> b
$ VarAnn -> VarAnn -> VarAnns
Un.TwoVarAnns VarAnn
vp VarAnn
vs
           in Instr c d -> Instr c d
withNotes (Instr c d -> Instr c d)
-> (Instr c d -> Instr c d) -> Instr c d -> Instr c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr c d -> Instr c d
withVarNotes (Instr c d -> Instr c d)
-> (Instr c d -> Instr c d) -> Instr c d -> Instr c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr c d -> Instr c d
withVarNotes' (Instr c d -> Instr c d) -> Instr c d -> Instr c d
forall a b. (a -> b) -> a -> b
$ Instr c d
instr

      Instr c d
GET_AND_UPDATE -> case HST d
outputStack of
        ((Notes x
valNotes, Dict (WellTyped x)
_, VarAnn
valVarAnn) ::& (Notes x
mapNotes, Dict (WellTyped x)
_, VarAnn
mapVarAnn) ::& HST xs
_) ->
          let
              -- `GET_AND_UPDATE` can have one var ann argument (e.g. 'GET_AND_UPDATE @var'),
              -- which is applied to the 2nd element of the stack (the updated map).
              withVarNotes :: Instr c d -> Instr c d
withVarNotes = if VarAnn
mapVarAnn VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
forall k (a :: k). Annotation a
Un.noAnn then Instr c d -> Instr c d
forall a. a -> a
id else NonEmpty VarAnn -> Instr c d -> Instr c d
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
mapVarAnn)
              -- `GET_AND_UPDATE` puts two elements on the top of the stack, both of which
              -- can have type/field/var annotations.
              withNotes :: Instr c d -> Instr c d
withNotes = if Notes x -> Bool
forall (t :: T). SingI t => Notes t -> Bool
isStar Notes x
valNotes Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
&& Notes x -> Bool
forall (t :: T). SingI t => Notes t -> Bool
isStar Notes x
mapNotes then Instr c d -> Instr c d
forall a. a -> a
id else Proxy s
-> Rec Notes '[x, x]
-> Instr (GetOpKey c : UpdOpParams c : c : s) ('[x, x] ++ s)
-> Instr (GetOpKey c : UpdOpParams c : c : s) ('[x, x] ++ s)
forall (a :: [T]) (topElems :: [T]) (s :: [T]).
(RMap topElems, RecordToList topElems,
 ReifyConstraint Show Notes topElems,
 ReifyConstraint NFData Notes topElems, Each '[SingI] topElems) =>
Proxy s
-> Rec Notes topElems
-> Instr a (topElems ++ s)
-> Instr a (topElems ++ s)
InstrWithNotes Proxy s
forall k (t :: k). Proxy t
Proxy (Notes x
valNotes Notes x -> Rec Notes '[x] -> Rec Notes '[x, x]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Notes x
mapNotes Notes x -> Rec Notes '[] -> Rec Notes '[x]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Notes '[]
forall u (a :: u -> *). Rec a '[]
RNil)
              withVarNotes' :: Instr c d -> Instr c d
withVarNotes' = if VarAnn
valVarAnn VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
forall k (a :: k). Annotation a
Un.noAnn Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
&& VarAnn
mapVarAnn VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
forall k (a :: k). Annotation a
Un.noAnn then Instr c d -> Instr c d
forall a. a -> a
id else VarAnns -> Instr c d -> Instr c d
forall (a :: [T]) (b :: [T]). VarAnns -> Instr a b -> Instr a b
InstrWithVarAnns (VarAnns -> Instr c d -> Instr c d)
-> VarAnns -> Instr c d -> Instr c d
forall a b. (a -> b) -> a -> b
$ VarAnn -> VarAnn -> VarAnns
Un.TwoVarAnns VarAnn
valVarAnn VarAnn
mapVarAnn
          in  Instr c d -> Instr c d
withNotes (Instr c d -> Instr c d)
-> (Instr c d -> Instr c d) -> Instr c d -> Instr c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr c d -> Instr c d
withVarNotes (Instr c d -> Instr c d)
-> (Instr c d -> Instr c d) -> Instr c d -> Instr c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr c d -> Instr c d
withVarNotes' (Instr c d -> Instr c d) -> Instr c d -> Instr c d
forall a b. (a -> b) -> a -> b
$ Instr c d
instr

      Instr c d
DUP -> Instr c d
instr''
      DUPN PeanoNatural n
_ -> Instr c d
instr''
      PUSH Value' Instr t
_ -> Instr c d
instr''
      Instr c d
UNIT -> Instr c d
instr''
      Instr c d
SOME -> Instr c d
instr''
      Instr c d
NONE -> Instr c d
instr''
      AnnPAIR{} -> Instr c d
instr''
      AnnLEFT{} -> Instr c d
instr''
      AnnRIGHT{} -> Instr c d
instr''
      Instr c d
NIL -> Instr c d
instr''
      Instr c d
CONS -> Instr c d
instr''
      Instr c d
SIZE -> Instr c d
instr''
      MAP Instr (MapOpInp c : s) (b : s)
_ -> Instr c d
instr''
      Instr c d
MEM -> Instr c d
instr''
      Instr c d
EMPTY_SET -> Instr c d
instr''
      Instr c d
EMPTY_MAP -> Instr c d
instr''
      Instr c d
EMPTY_BIG_MAP -> Instr c d
instr''
      Instr c d
UPDATE -> Instr c d
instr''
      UPDATEN PeanoNatural ix
_ -> Instr c d
instr''
      Instr c d
GET -> Instr c d
instr''
      GETN PeanoNatural ix
_ -> Instr c d
instr''
      LAMBDA Value' Instr ('TLambda i o)
_ -> Instr c d
instr''
      Instr c d
EXEC -> Instr c d
instr''
      Instr c d
ADD -> Instr c d
instr''
      Instr c d
SUB -> Instr c d
instr''
      Instr c d
CONCAT -> Instr c d
instr''
      Instr c d
CONCAT' -> Instr c d
instr''
      Instr c d
MUL -> Instr c d
instr''
      Instr c d
OR -> Instr c d
instr''
      Instr c d
AND -> Instr c d
instr''
      Instr c d
XOR -> Instr c d
instr''
      Instr c d
NOT -> Instr c d
instr''
      Instr c d
ABS -> Instr c d
instr''
      Instr c d
ISNAT -> Instr c d
instr''
      Instr c d
INT -> Instr c d
instr''
      Instr c d
NEG -> Instr c d
instr''
      Instr c d
EDIV -> Instr c d
instr''
      Instr c d
LSL -> Instr c d
instr''
      Instr c d
LSR -> Instr c d
instr''
      Instr c d
COMPARE -> Instr c d
instr''
      Instr c d
EQ -> Instr c d
instr''
      Instr c d
NEQ -> Instr c d
instr''
      Instr c d
LT -> Instr c d
instr''
      Instr c d
GT -> Instr c d
instr''
      Instr c d
LE -> Instr c d
instr''
      Instr c d
GE -> Instr c d
instr''
      Instr c d
ADDRESS -> Instr c d
instr''
      CONTRACT Notes p
_ EpName
_ -> Instr c d
instr''
      Instr c d
SET_DELEGATE -> Instr c d
instr''
      Instr c d
IMPLICIT_ACCOUNT -> Instr c d
instr''
      Instr c d
NOW -> Instr c d
instr''
      Instr c d
LEVEL -> Instr c d
instr''
      Instr c d
AMOUNT -> Instr c d
instr''
      Instr c d
BALANCE -> Instr c d
instr''
      Instr c d
HASH_KEY -> Instr c d
instr''
      Instr c d
CHECK_SIGNATURE -> Instr c d
instr''
      Instr c d
BLAKE2B -> Instr c d
instr''
      Instr c d
SOURCE -> Instr c d
instr''
      Instr c d
SENDER -> Instr c d
instr''
      SELF SomeEntrypointCallT arg
_ -> Instr c d
instr''
      Instr c d
SELF_ADDRESS -> Instr c d
instr''
      Instr c d
CAST -> Instr c d
instr''
      Instr c d
RENAME -> Instr c d
instr''
      Instr c d
CHAIN_ID -> Instr c d
instr''
      Instr c d
APPLY -> Instr c d
instr''
      PAIRN PeanoNatural n
_ -> Instr c d
instr''
      Instr c d
PACK -> Instr c d
instr''
      Instr c d
UNPACK -> Instr c d
instr''
      Instr c d
SLICE -> Instr c d
instr''
      Instr c d
TRANSFER_TOKENS -> Instr c d
instr''
      Instr c d
VOTING_POWER -> Instr c d
instr''
      Instr c d
TOTAL_VOTING_POWER -> Instr c d
instr''
      Instr c d
SHA256 -> Instr c d
instr''
      Instr c d
SHA512 -> Instr c d
instr''
      Instr c d
SHA3 -> Instr c d
instr''
      Instr c d
KECCAK -> Instr c d
instr''
      Instr c d
PAIRING_CHECK -> Instr c d
instr''
      Instr c d
TICKET -> Instr c d
instr''
      Instr c d
READ_TICKET -> Instr c d
instr''
      Instr c d
SPLIT_TICKET -> Instr c d
instr''
      Instr c d
JOIN_TICKETS -> 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
        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
addNotesOneVarAnn HST d
outputStack Instr c d
instr

    addNotesOneVarAnn :: HST d -> Instr c d -> Instr c d
    addNotesOneVarAnn :: HST d -> Instr c d -> Instr c d
addNotesOneVarAnn HST d
outputStack Instr c d
instr = case HST d
outputStack of
      ((Notes x
n, Dict (WellTyped x)
_, VarAnn
v) ::& HST xs
_) ->
        let withNotes :: Instr c d -> Instr c d
withNotes = if Notes x -> Bool
forall (t :: T). SingI t => Notes t -> Bool
isStar Notes x
n then Instr c d -> Instr c d
forall a. a -> a
id else Proxy xs
-> Rec Notes '[x] -> Instr c ('[x] ++ xs) -> Instr c ('[x] ++ xs)
forall (a :: [T]) (topElems :: [T]) (s :: [T]).
(RMap topElems, RecordToList topElems,
 ReifyConstraint Show Notes topElems,
 ReifyConstraint NFData Notes topElems, Each '[SingI] topElems) =>
Proxy s
-> Rec Notes topElems
-> Instr a (topElems ++ s)
-> Instr a (topElems ++ s)
InstrWithNotes Proxy xs
forall k (t :: k). Proxy t
Proxy (Notes x
n Notes x -> Rec Notes '[] -> Rec Notes '[x]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Notes '[]
forall u (a :: u -> *). Rec a '[]
RNil)
            withVarNotes :: Instr c d -> Instr c d
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 d -> Instr c d
forall a. a -> a
id else NonEmpty VarAnn -> Instr c d -> Instr c d
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)
            withVarNotes' :: Instr c d -> Instr c d
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 d -> Instr c d
forall a. a -> a
id else VarAnns -> Instr c d -> Instr c d
forall (a :: [T]) (b :: [T]). VarAnns -> Instr a b -> Instr a b
InstrWithVarAnns (VarAnns -> Instr c d -> Instr c d)
-> VarAnns -> Instr c d -> Instr c d
forall a b. (a -> b) -> a -> b
$ VarAnn -> VarAnns
Un.OneVarAnn VarAnn
v
         in Instr c d -> Instr c d
withNotes (Instr c d -> Instr c d)
-> (Instr c d -> Instr c d) -> Instr c d -> Instr c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr c d -> Instr c d
withVarNotes (Instr c d -> Instr c d)
-> (Instr c d -> Instr c d) -> Instr c d -> Instr c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr c d -> Instr c d
withVarNotes' (Instr c d -> Instr c d) -> Instr c d -> Instr c d
forall a b. (a -> b) -> a -> b
$ Instr c d
instr
      HST d
SNil -> Instr c d
instr

    addNotesNoVarAnn :: HST d -> Instr c d -> Instr c d
    addNotesNoVarAnn :: HST d -> Instr c d -> Instr c d
addNotesNoVarAnn HST d
outputStack Instr c d
instr = case HST d
outputStack of
      ((Notes x
n, Dict (WellTyped x)
_, VarAnn
v) ::& HST xs
_) ->
          let withNotes :: Instr c d -> Instr c d
withNotes = if Notes x -> Bool
forall (t :: T). SingI t => Notes t -> Bool
isStar Notes x
n then Instr c d -> Instr c d
forall a. a -> a
id else Proxy xs
-> Rec Notes '[x] -> Instr c ('[x] ++ xs) -> Instr c ('[x] ++ xs)
forall (a :: [T]) (topElems :: [T]) (s :: [T]).
(RMap topElems, RecordToList topElems,
 ReifyConstraint Show Notes topElems,
 ReifyConstraint NFData Notes topElems, Each '[SingI] topElems) =>
Proxy s
-> Rec Notes topElems
-> Instr a (topElems ++ s)
-> Instr a (topElems ++ s)
InstrWithNotes Proxy xs
forall k (t :: k). Proxy t
Proxy (Notes x
n Notes x -> Rec Notes '[] -> Rec Notes '[x]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Notes '[]
forall u (a :: u -> *). Rec a '[]
RNil)
              withVarNotes' :: Instr c d -> Instr c d
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 d -> Instr c d
forall a. a -> a
id else VarAnns -> Instr c d -> Instr c d
forall (a :: [T]) (b :: [T]). VarAnns -> Instr a b -> Instr a b
InstrWithVarAnns (VarAnns -> Instr c d -> Instr c d)
-> VarAnns -> Instr c d -> Instr c d
forall a b. (a -> b) -> a -> b
$ VarAnn -> VarAnns
Un.OneVarAnn VarAnn
v
           in Instr c d -> Instr c d
withNotes (Instr c d -> Instr c d)
-> (Instr c d -> Instr c d) -> Instr c d -> Instr c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr c d -> Instr c d
withVarNotes' (Instr c d -> Instr c d) -> Instr c d -> Instr c d
forall a b. (a -> b) -> a -> b
$ Instr c d
instr
      HST d
SNil -> Instr c d
instr

-- | Like 'typeCheckImpl' but doesn't add a stack type comment after the
-- sequence.
typeCheckImplNoLastTypeComment
  :: forall inp . SingI inp
  => TcInstrHandler
  -> [Un.ExpandedOp]
  -> HST inp
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment :: TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment TcInstrHandler
_ [] 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]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST inp
inputStack))
typeCheckImplNoLastTypeComment TcInstrHandler
tcInstr [ExpandedOp
op] HST inp
inputStack = do
  TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI 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 TcInstrHandler
tcInstr (ExpandedOp
op : [ExpandedOp]
ops) HST inp
inputStack = do
  TypeCheckedSeq inp
done <- TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op HST inp
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 TcInstrHandler
tcInstr TypeCheckedSeq inp
done [ExpandedOp]
rest = case TypeCheckedSeq inp
done of
  WellTypedSeq SomeInstr inp
instr -> SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
handleFirst SomeInstr inp
instr
  MixedSeq SomeInstr inp
i TCError
e [IllTypedInstr]
left -> TypeCheckedSeq inp -> 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 TCError
e [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@(HST inp
inputStack :/ SomeInstrOut inp
instrAndOutputStack) = do
      case SomeInstrOut inp
instrAndOutputStack of
        Instr inp out
instr ::: HST out
outputStack -> do
          TypeCheckedSeq out
nextPiece <- TcInstrHandler
-> [ExpandedOp]
-> HST out
-> TypeCheckInstrNoExcept (TypeCheckedSeq out)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment TcInstrHandler
tcInstr [ExpandedOp]
rest HST out
outputStack
          let combiner :: SomeInstr out -> SomeInstr inp
combiner = HST inp -> Instr inp out -> SomeInstr out -> SomeInstr inp
forall (inp :: [T]) (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 SomeInstr out
nextInstr -> SomeInstr inp -> TypeCheckedSeq inp
forall (inp :: [T]). SomeInstr inp -> TypeCheckedSeq inp
WellTypedSeq (SomeInstr out -> SomeInstr inp
combiner SomeInstr out
nextInstr)
            MixedSeq SomeInstr out
nextInstr TCError
err [IllTypedInstr]
left -> SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
forall (inp :: [T]).
SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
MixedSeq (SomeInstr out -> SomeInstr inp
combiner SomeInstr out
nextInstr) TCError
err [IllTypedInstr]
left
            IllTypedSeq TCError
err [IllTypedInstr]
left -> SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
forall (inp :: [T]).
SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
MixedSeq SomeInstr inp
packedInstr TCError
err [IllTypedInstr]
left
        AnyOutInstr{} -> TypeCheckedSeq inp -> 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
          ExpandedOp
op : [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 HST inp
inp Instr inp out
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 HST inp
inp Instr inp out
i1 (HST out
_ :/ 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 InstrCallStack
loc ExpandedOp
_) = InstrCallStack
loc
    extractOpPos ExpandedOp
_ = 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 . SingI inp
  => TcInstrHandler
  -> [Un.ExpandedOp]
  -> HST inp
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplStripped :: TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplStripped TcInstrHandler
tcInstr [] HST inp
inp
  = TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment TcInstrHandler
tcInstr [] HST inp
inp
typeCheckImplStripped TcInstrHandler
tcInstr (ExpandedOp
op : [ExpandedOp]
ops) HST inp
inp = do
  TypeCheckedSeq inp
done <- TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op HST inp
inp
  TcInstrHandler
-> TypeCheckedSeq inp
-> [ExpandedOp]
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
TcInstrHandler
-> TypeCheckedSeq inp
-> [ExpandedOp]
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
continueTypeChecking TcInstrHandler
tcInstr TypeCheckedSeq inp
done [ExpandedOp]
ops

typeCheckImpl
  :: forall inp . SingI inp
  => TcInstrHandler
  -> [Un.ExpandedOp]
  -> HST inp
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl :: TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl TcInstrHandler
tcInstr [ExpandedOp]
ops HST inp
inputStack = do
  TypeCheckedSeq inp
tcSeq <- TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment TcInstrHandler
tcInstr [ExpandedOp]
ops HST inp
inputStack
  (SomeInstr inp
 -> ReaderT 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@(HST inp
inp :/ 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
        (Bool
True, Instr inp out
i ::: HST out
out) -> HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ Instr inp out -> Instr out out -> Instr inp out
forall (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]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST out
out
        (Bool
True, AnyOutInstr forall (out :: [T]). Instr inp out
i) -> HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ (forall (out :: [T]). Instr inp out) -> SomeInstrOut inp
forall (inp :: [T]).
(forall (out :: [T]). Instr inp out) -> SomeInstrOut inp
AnyOutInstr (Instr inp out -> Instr out out -> Instr inp out
forall (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)
        (Bool, SomeInstrOut inp)
_ -> SomeInstr inp
packedI


prependStackTypeComment
  :: SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp)
prependStackTypeComment :: SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp)
prependStackTypeComment packedInstr :: SomeInstr inp
packedInstr@(HST inp
inp :/ SomeInstrOut 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
forall a. Boolean a => a -> a -> a
&& (Bool -> Bool
not (SomeInstr inp -> Bool
forall (inp :: [T]). SomeInstr inp -> Bool
isNop' SomeInstr inp
packedInstr))
    then (forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeInstr inp -> SomeInstr inp
forall (inp :: [T]).
(forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeInstr inp -> SomeInstr inp
mapSomeInstr (Instr inp inp -> Instr inp out -> Instr inp out
forall (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' (HST inp
_ :/ Instr inp out
i ::: HST out
_) = Instr inp out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp out
i
isNop' (HST inp
_ :/ AnyOutInstr forall (out :: [T]). Instr inp out
i) = Instr inp Any -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp Any
forall (out :: [T]). Instr inp out
i

isNop :: Instr inp out -> Bool
isNop :: Instr inp out -> Bool
isNop (WithLoc InstrCallStack
_ Instr inp out
i) = Instr inp out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp out
i
isNop (InstrWithNotes Proxy s
_ Rec Notes topElems
_ Instr inp (topElems ++ s)
i) = Instr inp out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp out
Instr inp (topElems ++ s)
i
isNop (InstrWithVarNotes NonEmpty VarAnn
_ Instr inp out
i) = Instr inp out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp out
i
isNop (FrameInstr Proxy s
_ Instr a b
i) = Instr a b -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr a b
i
isNop (Seq Instr inp b
i1 Instr b out
i2) = Instr inp b -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp b
i1 Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
&& Instr b out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr b out
i2
isNop (Nested Instr inp out
i) = Instr inp out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp out
i
isNop Instr inp out
Nop = Bool
True
isNop (Ext ExtInstr inp
_) = Bool
True
isNop Instr inp out
_ = Bool
False

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

mapSeq
  :: (SomeInstr inp -> SomeInstr inp')
  -> TypeCheckedSeq inp
  -> TypeCheckedSeq inp'
mapSeq :: (SomeInstr inp -> SomeInstr inp')
-> TypeCheckedSeq inp -> TypeCheckedSeq inp'
mapSeq SomeInstr inp -> SomeInstr inp'
f = Identity (TypeCheckedSeq inp') -> TypeCheckedSeq inp'
forall a. Identity a -> a
runIdentity (Identity (TypeCheckedSeq inp') -> TypeCheckedSeq inp')
-> (TypeCheckedSeq inp -> Identity (TypeCheckedSeq inp'))
-> TypeCheckedSeq inp
-> TypeCheckedSeq inp'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SomeInstr inp -> Identity (SomeInstr inp'))
-> TypeCheckedSeq inp -> Identity (TypeCheckedSeq inp')
forall (f :: * -> *) (inp :: [T]) (inp' :: [T]).
Applicative f =>
(SomeInstr inp -> f (SomeInstr inp'))
-> TypeCheckedSeq inp -> f (TypeCheckedSeq inp')
mapMSeq (SomeInstr inp' -> Identity (SomeInstr inp')
forall a. a -> Identity a
Identity (SomeInstr inp' -> Identity (SomeInstr inp'))
-> (SomeInstr inp -> SomeInstr inp')
-> SomeInstr inp
-> Identity (SomeInstr inp')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeInstr inp -> SomeInstr inp'
f)

stackTypeComment :: HST st -> Instr st st
stackTypeComment :: 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 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 inp
someInstr -> case SomeInstr inp
someInstr of
  (HST inp
_ :/ WithLoc{} ::: HST out
_) -> SomeInstr inp
someInstr
  (HST inp
inp :/ Instr inp out
instr ::: HST out
out) -> HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ 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]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST out
out
  (HST inp
inp :/ AnyOutInstr forall (out :: [T]). Instr inp out
instr) -> HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ ((forall (out :: [T]). Instr inp out) -> SomeInstrOut inp
forall (inp :: [T]).
(forall (out :: [T]). Instr inp out) -> SomeInstrOut inp
AnyOutInstr ((forall (out :: [T]). Instr inp out) -> SomeInstrOut inp)
-> (forall (out :: [T]). Instr inp out) -> SomeInstrOut inp
forall a b. (a -> b) -> a -> b
$ 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 '[SingI] [t1, t2])
  => Notes t1 -> Notes t2 -> Either TCTypeError (t1 :~: t2, Notes t1)
matchTypes :: Notes t1 -> Notes t2 -> Either TCTypeError (t1 :~: t2, Notes t1)
matchTypes Notes t1
n1 Notes t2
n2 = do
  t1 :~: t2
Refl <- Each '[SingI] '[t1, t2] => Either TCTypeError (t1 :~: t2)
forall (a :: T) (b :: T).
Each '[SingI] '[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
    , SingI (MemOpKey c)
    , inp ~ (memKey : c : rs)
    , SingI 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 Notes (MemOpKey c)
cKeyNotes inputHST :: HST inp
inputHST@((Notes x, Dict (WellTyped x), VarAnn)
hst0 ::& (Notes x, Dict (WellTyped x), VarAnn)
_ ::& HST xs
hstTail) VarAnn
varAnn =
  case Each '[SingI] '[memKey, MemOpKey c] =>
Either TCTypeError (memKey :~: MemOpKey c)
forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @memKey @(MemOpKey c) of
    Right memKey :~: MemOpKey c
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, SingI 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]).
SingI 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 (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
hstTail)
    Left 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]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) TCTypeError
m
  where
    (Notes x
memKeyNotes, Dict (WellTyped x)
Dict, VarAnn
_) = (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, SingI (GetOpKey c)
    , WellTyped (GetOpVal c)
    , inp ~ (getKey : c : rs)
    , SingI 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 Notes (GetOpKey c)
notesKeyC inputHST :: HST inp
inputHST@((Notes x, Dict (WellTyped x), VarAnn)
hst0 ::& (Notes x, Dict (WellTyped x), VarAnn)
_ ::& HST xs
hstTail) Notes (GetOpVal c)
valueNotes VarAnn
varAnn =
  case Each '[SingI] '[getKey, GetOpKey c] =>
Either TCTypeError (getKey :~: GetOpKey c)
forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @getKey @(GetOpKey c) of
    Right getKey :~: GetOpKey c
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, SingI 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) (s :: [T]).
(GetOp c, SingI (GetOpVal c)) =>
Instr (GetOpKey c : c : s) ('TOption (GetOpVal c) : s)
GET Instr inp ('TOption (GetOpVal c) : xs)
-> HST ('TOption (GetOpVal c) : xs) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((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 (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
hstTail)
    Left 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]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) TCTypeError
m
  where
    (Notes x
getKeyNotes, Dict (WellTyped x)
Dict, VarAnn
_) = (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
    , SingI (UpdOpKey c), SingI (UpdOpParams c)
    , SingI rs
    , 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 Notes (UpdOpKey c)
cKeyNotes inputHST :: HST inp
inputHST@((Notes x, Dict (WellTyped x), VarAnn)
hst0 ::& (Notes x, Dict (WellTyped x), VarAnn)
hst1 ::& (Notes x, Dict (WellTyped x), VarAnn)
cTuple ::& HST xs
hstTail) Notes (UpdOpParams c)
cValueNotes VarAnn
varAnn =
  case (Each '[SingI] '[updKey, UpdOpKey c] =>
Either TCTypeError (updKey :~: UpdOpKey c)
forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @updKey @(UpdOpKey c), Each '[SingI] '[updParams, UpdOpParams c] =>
Either TCTypeError (updParams :~: UpdOpParams c)
forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @updParams @(UpdOpParams c)) of
    (Right updKey :~: UpdOpKey c
Refl, Right 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, SingI 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, SingI 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)
      let vn :: VarAnn
vn = VarAnn
varAnn VarAnn -> VarAnn -> VarAnn
forall k (t :: k). Annotation t -> Annotation t -> Annotation t
`orAnn` ((Notes x, Dict (WellTyped x), VarAnn)
cTuple (Notes x, Dict (WellTyped x), VarAnn)
-> Getting VarAnn (Notes x, Dict (WellTyped x), VarAnn) VarAnn
-> VarAnn
forall s a. s -> Getting a s a -> a
^. Getting VarAnn (Notes x, Dict (WellTyped x), VarAnn) VarAnn
forall s t a b. Field3 s t a b => Lens s t a b
_3)
      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]).
SingI 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
vn) (Notes c, Dict (WellTyped c), VarAnn) -> HST xs -> HST (c : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
hstTail)
    (Left TCTypeError
m, Either TCTypeError (updParams :~: UpdOpParams c)
_) ->
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) TCTypeError
m
    (Either TCTypeError (updKey :~: UpdOpKey c)
_, Left TCTypeError
m) ->
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerValueType) TCTypeError
m
  where
    (Notes x
updKeyNotes, Dict (WellTyped x)
Dict, VarAnn
_) = (Notes x, Dict (WellTyped x), VarAnn)
hst0
    (Notes x
updValueNotes, Dict (WellTyped x)
Dict, VarAnn
_) = (Notes x, Dict (WellTyped x), VarAnn)
hst1
    uInstr :: ExpandedInstr
uInstr = VarAnn -> ExpandedInstr
forall op. VarAnn -> InstrAbstract op
Un.UPDATE VarAnn
varAnn

getUpdImpl
  :: forall c updKey updParams rs inp m .
    ( UpdOp c, GetOp c
    , SingI (UpdOpKey c)
    , SingI (GetOpVal c)
    , inp ~ (updKey : updParams : c : rs)
    , SingI rs
    , GetOpKey c ~ UpdOpKey c
    , UpdOpParams c ~ 'TOption (GetOpVal c)
    , MonadReader InstrCallStack m
    , MonadError TCError m
    )
  => Notes (UpdOpKey c)
  -> HST inp
  -> Notes (UpdOpParams c)
  -> VarAnn
  -> m (SomeInstr inp)
getUpdImpl :: Notes (UpdOpKey c)
-> HST inp -> Notes (UpdOpParams c) -> VarAnn -> m (SomeInstr inp)
getUpdImpl Notes (UpdOpKey c)
cKeyNotes inputHST :: HST inp
inputHST@((Notes x, Dict (WellTyped x), VarAnn)
hst0 ::& (Notes x, Dict (WellTyped x), VarAnn)
hst1 ::& (Notes x, Dict (WellTyped x), VarAnn)
cTuple ::& HST xs
hstTail) Notes (UpdOpParams c)
cValueNotes VarAnn
varAnn =
  case (Each '[SingI] '[updKey, UpdOpKey c] =>
Either TCTypeError (updKey :~: UpdOpKey c)
forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @updKey @(UpdOpKey c), Each '[SingI] '[updParams, UpdOpParams c] =>
Either TCTypeError (updParams :~: UpdOpParams c)
forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @updParams @(UpdOpParams c)) of
    (Right updKey :~: UpdOpKey c
Refl, Right 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, SingI 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, SingI 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)
      let vn :: VarAnn
vn = VarAnn
varAnn VarAnn -> VarAnn -> VarAnn
forall k (t :: k). Annotation t -> Annotation t -> Annotation t
`orAnn` ((Notes x, Dict (WellTyped x), VarAnn)
cTuple (Notes x, Dict (WellTyped x), VarAnn)
-> Getting VarAnn (Notes x, Dict (WellTyped x), VarAnn) VarAnn
-> VarAnn
forall s a. s -> Getting a s a -> a
^. Getting VarAnn (Notes x, Dict (WellTyped x), VarAnn) VarAnn
forall s t a b. Field3 s t a b => Lens s t a b
_3)
      pure $ HST inp
inputHST HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/
        Instr inp (x : c : xs)
forall (c :: T) (s :: [T]).
(GetOp c, UpdOp c, SingI (GetOpVal c), UpdOpKey c ~ GetOpKey c) =>
Instr
  (UpdOpKey c : UpdOpParams c : c : s)
  ('TOption (GetOpVal c) : c : s)
GET_AND_UPDATE Instr inp (x : c : xs) -> HST (x : c : xs) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Notes x, Dict (WellTyped x), VarAnn)
hst1 (Notes x, Dict (WellTyped x), VarAnn)
-> HST (c : xs) -> HST (x : c : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& ((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
vn) (Notes c, Dict (WellTyped c), VarAnn) -> HST xs -> HST (c : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
hstTail)
    (Left TCTypeError
m, Either TCTypeError (updParams :~: 'TOption (GetOpVal c))
_) ->
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) TCTypeError
m
    (Either TCTypeError (updKey :~: UpdOpKey c)
_, Left TCTypeError
m) ->
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerValueType) TCTypeError
m
  where
    (Notes x
updKeyNotes, Dict (WellTyped x)
Dict, VarAnn
_) = (Notes x, Dict (WellTyped x), VarAnn)
hst0
    (Notes x
updValueNotes, Dict (WellTyped x)
Dict, VarAnn
_) = (Notes x, Dict (WellTyped x), VarAnn)
hst1
    uInstr :: ExpandedInstr
uInstr = VarAnn -> ExpandedInstr
forall op. VarAnn -> InstrAbstract op
Un.GET_AND_UPDATE VarAnn
varAnn

sizeImpl
  :: (SizeOp c, inp ~ (c ': rs), Monad m)
  => HST inp
  -> VarAnn
  -> m (SomeInstr inp)
sizeImpl :: HST inp -> VarAnn -> m (SomeInstr inp)
sizeImpl i :: HST inp
i@((Notes x, Dict (WellTyped x), VarAnn)
_ ::& HST xs
rs) VarAnn
vn =
  SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ 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]).
SingI 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 (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs)

sliceImpl
  :: (SliceOp c, inp ~ ('TNat ': 'TNat ': c ': rs), Monad m)
  => HST inp
  -> Un.VarAnn
  -> m (SomeInstr inp)
sliceImpl :: HST inp -> VarAnn -> m (SomeInstr inp)
sliceImpl i :: HST inp
i@((Notes x, Dict (WellTyped x), VarAnn)
_ ::& (Notes x, Dict (WellTyped x), VarAnn)
_ ::& (Notes x
cn, Dict (WellTyped x)
Dict, VarAnn
cvn) ::& HST xs
rs) 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 [annQ|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, SingI 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]).
SingI 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 (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(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 TypeAnn
_ Notes t
n, Dict (WellTyped x)
Dict, VarAnn
_) ::& HST xs
rs) VarAnn
vn = do
  SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ 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]).
SingI 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 (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(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@((Notes x
cn1, Dict (WellTyped x)
_, VarAnn
_) ::& (Notes x
cn2, Dict (WellTyped x)
_, VarAnn
_) ::& HST xs
rs) 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, SingI 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]).
SingI 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 (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(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
     , 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 Instr inp (ArithRes aop n m : s)
mkInstr i :: HST inp
i@((Notes x
an, Dict (WellTyped x)
_, VarAnn
_) ::& (Notes x
bn, Dict (WellTyped x)
_, VarAnn
_) ::& HST xs
rs) VarAnn
vn 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 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]).
SingI 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 (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs)
    Left 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]). SingI 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.
     ( Each '[SingI] [a, b]
     , inp ~ (a ': b ': rs)
     , SingI 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 Sing a
t1 Sing b
t2 = case (Sing a
SingT a
t1, Sing b
SingT b
t2) of
  (SingT a
STInt, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  (SingT a
STInt, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  (SingT a
STNat, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  (SingT a
STNat, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  (SingT a
STInt, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  (SingT a
STTimestamp, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  (SingT a
STMutez, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  (SingT a
STBls12381Fr, SingT b
STBls12381Fr) -> Instr
  ('TBls12381Fr : 'TBls12381Fr : rs)
  (ArithRes Add 'TBls12381Fr 'TBls12381Fr : rs)
-> HST ('TBls12381Fr : 'TBls12381Fr : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TBls12381Fr : 'TBls12381Fr : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, 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
  ('TBls12381Fr : 'TBls12381Fr : rs)
  (ArithRes Add 'TBls12381Fr 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  (SingT a
STBls12381G1, SingT b
STBls12381G1) -> Instr
  ('TBls12381G1 : 'TBls12381G1 : rs)
  (ArithRes Add 'TBls12381G1 'TBls12381G1 : rs)
-> HST ('TBls12381G1 : 'TBls12381G1 : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TBls12381G1 : 'TBls12381G1 : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, 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
  ('TBls12381G1 : 'TBls12381G1 : rs)
  (ArithRes Add 'TBls12381G1 'TBls12381G1 : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  (SingT a
STBls12381G2, SingT b
STBls12381G2) -> Instr
  ('TBls12381G2 : 'TBls12381G2 : rs)
  (ArithRes Add 'TBls12381G2 'TBls12381G2 : rs)
-> HST ('TBls12381G2 : 'TBls12381G2 : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TBls12381G2 : 'TBls12381G2 : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, 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
  ('TBls12381G2 : 'TBls12381G2 : rs)
  (ArithRes Add 'TBls12381G2 'TBls12381G2 : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  (SingT a, SingT b)
_ -> \HST inp
i VarAnn
_ 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]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TCTypeError -> m (SomeInstr inp))
-> TCTypeError -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$
    T -> T -> TCTypeError
NotNumericTypes ((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.
     ( SingI rs
     , Each '[SingI] [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 Sing a
t1 Sing b
t2 = case (Sing a
SingT a
t1, Sing b
SingT b
t2) of
  (SingT a
STInt, SingT b
STInt) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(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
  (SingT a
STInt, SingT b
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
  (SingT a
STNat, SingT b
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
  (SingT a
STNat, SingT b
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
  (SingT a
STMutez, SingT b
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
  (SingT a
STMutez, SingT b
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
  (SingT a, SingT b)
_ -> \HST inp
i VarAnn
_ 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]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TCTypeError -> m (SomeInstr inp))
-> TCTypeError -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$
    T -> T -> TCTypeError
NotNumericTypes ((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@((Notes x
an, Dict (WellTyped x)
_, VarAnn
_) ::& (Notes x
bn, Dict (WellTyped x)
_, VarAnn
_) ::& HST xs
rs) VarAnn
vn 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 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]).
SingI 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 (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs)
    Left 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]). SingI 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.
     ( Each '[SingI] [a, b]
     , inp ~ (a ': b ': rs)
     , SingI 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 Sing a
t1 Sing b
t2 = case (Sing a
SingT a
t1, Sing b
SingT b
t2) of
  (SingT a
STInt, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Sub n m : s)
SUB
  (SingT a
STInt, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Sub n m : s)
SUB
  (SingT a
STNat, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Sub n m : s)
SUB
  (SingT a
STNat, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Sub n m : s)
SUB
  (SingT a
STTimestamp, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Sub n m : s)
SUB
  (SingT a
STTimestamp, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Sub n m : s)
SUB
  (SingT a
STMutez, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Sub n m : s)
SUB
  (SingT a, SingT b)
_ -> \HST inp
i VarAnn
_ 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]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TCTypeError -> m (SomeInstr inp))
-> TCTypeError -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$
    T -> T -> TCTypeError
NotNumericTypes ((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.
     ( Each '[SingI] [a, b]
     , inp ~ (a ': b ': rs)
     , SingI 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 Sing a
t1 Sing b
t2 = case (Sing a
SingT a
t1, Sing b
SingT b
t2) of
  (SingT a
STInt, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (SingT a
STInt, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (SingT a
STNat, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (SingT a
STNat, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (SingT a
STNat, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (SingT a
STMutez, SingT b
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, 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 =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (SingT a
STInt, SingT b
STBls12381Fr) -> Instr
  ('TInt : 'TBls12381Fr : rs) (ArithRes Mul 'TInt 'TBls12381Fr : rs)
-> HST ('TInt : 'TBls12381Fr : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TInt : 'TBls12381Fr : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, 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 : 'TBls12381Fr : rs) (ArithRes Mul 'TInt 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (SingT a
STNat, SingT b
STBls12381Fr) -> Instr
  ('TNat : 'TBls12381Fr : rs) (ArithRes Mul 'TNat 'TBls12381Fr : rs)
-> HST ('TNat : 'TBls12381Fr : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TNat : 'TBls12381Fr : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, 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 : 'TBls12381Fr : rs) (ArithRes Mul 'TNat 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (SingT a
STBls12381Fr, SingT b
STInt) -> Instr
  ('TBls12381Fr : 'TInt : rs) (ArithRes Mul 'TBls12381Fr 'TInt : rs)
-> HST ('TBls12381Fr : 'TInt : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TBls12381Fr : 'TInt : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, 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
  ('TBls12381Fr : 'TInt : rs) (ArithRes Mul 'TBls12381Fr 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (SingT a
STBls12381Fr, SingT b
STNat) -> Instr
  ('TBls12381Fr : 'TNat : rs) (ArithRes Mul 'TBls12381Fr 'TNat : rs)
-> HST ('TBls12381Fr : 'TNat : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TBls12381Fr : 'TNat : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, 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
  ('TBls12381Fr : 'TNat : rs) (ArithRes Mul 'TBls12381Fr 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (SingT a
STBls12381Fr, SingT b
STBls12381Fr) -> Instr
  ('TBls12381Fr : 'TBls12381Fr : rs)
  (ArithRes Mul 'TBls12381Fr 'TBls12381Fr : rs)
-> HST ('TBls12381Fr : 'TBls12381Fr : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TBls12381Fr : 'TBls12381Fr : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, 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
  ('TBls12381Fr : 'TBls12381Fr : rs)
  (ArithRes Mul 'TBls12381Fr 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (SingT a
STBls12381G1, SingT b
STBls12381Fr) -> Instr
  ('TBls12381G1 : 'TBls12381Fr : rs)
  (ArithRes Mul 'TBls12381G1 'TBls12381Fr : rs)
-> HST ('TBls12381G1 : 'TBls12381Fr : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TBls12381G1 : 'TBls12381Fr : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, 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
  ('TBls12381G1 : 'TBls12381Fr : rs)
  (ArithRes Mul 'TBls12381G1 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (SingT a
STBls12381G2, SingT b
STBls12381Fr) -> Instr
  ('TBls12381G2 : 'TBls12381Fr : rs)
  (ArithRes Mul 'TBls12381G2 'TBls12381Fr : rs)
-> HST ('TBls12381G2 : 'TBls12381Fr : rs)
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr ('TBls12381G2 : 'TBls12381Fr : rs))
forall k (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
       (t :: * -> *).
(ArithOp aop n m, 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
  ('TBls12381G2 : 'TBls12381Fr : rs)
  (ArithRes Mul 'TBls12381G2 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  (SingT a, SingT b)
_ -> \HST inp
i VarAnn
_ 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]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TCTypeError -> m (SomeInstr inp))
-> TCTypeError -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$
    T -> T -> TCTypeError
NotNumericTypes ((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
  :: ( 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 Instr inp (UnaryArithRes aop n : s)
mkInstr i :: HST inp
i@((Notes x, Dict (WellTyped x), VarAnn)
_ ::& HST xs
rs) 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]).
SingI 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 (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(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
  :: ( 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 Instr inp (UnaryArithRes aop n : s)
mkInstr i :: HST inp
i@((Notes x
n, Dict (WellTyped x)
_, VarAnn
_) ::& HST xs
rs) 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]).
SingI 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 (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs)