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

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

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

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

import Prelude hiding (EQ, GT, LT)

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

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

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

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

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

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

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

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

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

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

-- TODO move to Util module
onLeft :: Either a c -> (a -> b) -> Either b c
onLeft :: Either a c -> (a -> b) -> Either b c
onLeft = ((a -> b) -> Either a c -> Either b c)
-> Either a c -> (a -> b) -> Either b c
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first

-- | Extract singleton for each single type of the given stack.
hstToTs :: HST st -> [T]
hstToTs :: HST st -> [T]
hstToTs = \case
  SNil -> []
  (notes :: Notes x
notes, _, _) ::& hst :: HST xs
hst -> Notes x -> T
forall (t :: T). SingI t => Notes t -> T
notesT Notes x
notes T -> [T] -> [T]
forall a. a -> [a] -> [a]
: HST xs -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST xs
hst

-- | Check whether the given stack types are equal.
eqHST
  :: forall as bs.
      (Typeable as, Typeable bs)
  => HST as -> HST bs -> Either TCTypeError (as :~: bs)
eqHST :: HST as -> HST bs -> Either TCTypeError (as :~: bs)
eqHST (HST as
hst :: HST xs) (HST bs
hst' :: HST ys) = do
  case (Typeable as, Typeable bs) => Maybe (as :~: bs)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @as @bs of
    Nothing -> TCTypeError -> Either TCTypeError (as :~: bs)
forall a b. a -> Either a b
Left (TCTypeError -> Either TCTypeError (as :~: bs))
-> TCTypeError -> Either TCTypeError (as :~: bs)
forall a b. (a -> b) -> a -> b
$ [T] -> [T] -> TCTypeError
StackEqError (HST as -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST as
hst) (HST bs -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST bs
hst')
    Just Refl -> do
      Either TCTypeError (HST as) -> Either TCTypeError ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Either TCTypeError (HST as) -> Either TCTypeError ())
-> Either TCTypeError (HST as) -> Either TCTypeError ()
forall a b. (a -> b) -> a -> b
$ HST as -> HST as -> Either AnnConvergeError (HST as)
forall (ts :: [T]).
HST ts -> HST ts -> Either AnnConvergeError (HST ts)
convergeHST HST as
hst HST as
HST bs
hst' Either AnnConvergeError (HST as)
-> (AnnConvergeError -> TCTypeError) -> Either TCTypeError (HST as)
forall a c b. Either a c -> (a -> b) -> Either b c
`onLeft` AnnConvergeError -> TCTypeError
AnnError
      return as :~: bs
forall k (a :: k). a :~: a
Refl

-- | Check whether the given stack has size 1 and its only element matches the
-- given type. This function is a specialized version of `eqHST`.
eqHST1
  :: forall t st.
      (Typeable st, WellTyped t)
  => HST st -> Either TCTypeError (st :~: '[t])
eqHST1 :: HST st -> Either TCTypeError (st :~: '[t])
eqHST1 hst :: HST st
hst = do
  let hst' :: HST '[t]
hst' = SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @t Sing t -> HST '[] -> HST '[t]
forall (xs :: [T]) (x :: T).
(Typeable xs, WellTyped x) =>
Sing x -> HST xs -> HST (x : xs)
-:& HST '[]
SNil
  case (Typeable '[t], Typeable st) => Maybe ('[t] :~: st)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @'[t] @st of
    Nothing -> TCTypeError -> Either TCTypeError (st :~: '[t])
forall a b. a -> Either a b
Left (TCTypeError -> Either TCTypeError (st :~: '[t]))
-> TCTypeError -> Either TCTypeError (st :~: '[t])
forall a b. (a -> b) -> a -> b
$ [T] -> [T] -> TCTypeError
StackEqError (HST '[t] -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST '[t]
hst') (HST st -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST st
hst)
    Just Refl -> (st :~: st) -> Either TCTypeError (st :~: st)
forall a b. b -> Either a b
Right st :~: st
forall k (a :: k). a :~: a
Refl

lengthHST :: HST xs -> Natural
lengthHST :: HST xs -> Natural
lengthHST (_ ::& xs :: HST xs
xs) = 1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ HST xs -> Natural
forall (xs :: [T]). HST xs -> Natural
lengthHST HST xs
xs
lengthHST SNil = 0

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

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

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

onTypeCheckInstrErr
  :: (MonadReader InstrCallStack m, MonadError TCError m)
  => Un.ExpandedInstr -> SomeHST -> Maybe TypeContext
  -> Either TCTypeError a -> m a
onTypeCheckInstrErr :: ExpandedInstr
-> SomeHST -> Maybe TypeContext -> Either TCTypeError a -> m a
onTypeCheckInstrErr instr :: ExpandedInstr
instr hst :: SomeHST
hst mContext :: Maybe TypeContext
mContext ei :: Either TCTypeError a
ei = do
  (TCTypeError -> m a) -> (a -> m a) -> Either TCTypeError a -> m a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
instr SomeHST
hst Maybe TypeContext
mContext) a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Either TCTypeError a
ei

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

typeCheckInstrErr
  :: (MonadReader InstrCallStack m, MonadError TCError m)
  => Un.ExpandedInstr -> SomeHST -> Maybe TypeContext
  -> m a
typeCheckInstrErr :: ExpandedInstr -> SomeHST -> Maybe TypeContext -> m a
typeCheckInstrErr instr :: ExpandedInstr
instr hst :: SomeHST
hst mContext :: Maybe TypeContext
mContext = do
  InstrCallStack
pos <- m InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
  TCError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> m a) -> TCError -> m a
forall a b. (a -> b) -> a -> b
$ ExpandedInstr
-> SomeHST
-> InstrCallStack
-> Maybe TypeContext
-> Maybe TCTypeError
-> TCError
TCFailedOnInstr ExpandedInstr
instr SomeHST
hst InstrCallStack
pos Maybe TypeContext
mContext Maybe TCTypeError
forall a. Maybe a
Nothing

typeCheckInstrErr'
  :: (MonadReader InstrCallStack m, MonadError TCError m)
  => Un.ExpandedInstr -> SomeHST -> Maybe TypeContext
  -> TCTypeError -> m a
typeCheckInstrErr' :: ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' instr :: ExpandedInstr
instr hst :: SomeHST
hst mContext :: Maybe TypeContext
mContext err :: TCTypeError
err = do
  InstrCallStack
pos <- m InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
  TCError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> m a) -> TCError -> m a
forall a b. (a -> b) -> a -> b
$ ExpandedInstr
-> SomeHST
-> InstrCallStack
-> Maybe TypeContext
-> Maybe TCTypeError
-> TCError
TCFailedOnInstr ExpandedInstr
instr SomeHST
hst InstrCallStack
pos Maybe TypeContext
mContext (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just TCTypeError
err)

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

withCompareableCheck
  :: forall a m v ts. (Typeable ts, MonadReader InstrCallStack m, MonadError TCError m)
  => Sing a
  -> Un.ExpandedInstr
  -> HST ts
  -> (Comparable a => v)
  -> m v
withCompareableCheck :: Sing a -> ExpandedInstr -> HST ts -> (Comparable a => v) -> m v
withCompareableCheck sng :: Sing a
sng instr :: ExpandedInstr
instr i :: HST ts
i act :: Comparable a => v
act = case Sing a -> Maybe (Dict (Comparable a))
forall (a :: T). Sing a -> Maybe (Dict (Comparable a))
getComparableProofS Sing a
sng of
  Just d :: Dict (Comparable a)
d@Dict (Comparable a)
Dict -> v -> m v
forall (f :: * -> *) a. Applicative f => a -> f a
pure (v -> m v) -> v -> m v
forall a b. (a -> b) -> a -> b
$ Dict (Comparable a) -> (Comparable a => v) -> v
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict Dict (Comparable a)
d Comparable a => v
act
  Nothing -> ExpandedInstr -> SomeHST -> Maybe TypeContext -> m v
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> m a
typeCheckInstrErr ExpandedInstr
instr (HST ts -> SomeHST
forall (ts :: [T]). Typeable ts => HST ts -> SomeHST
SomeHST HST ts
i) (Maybe TypeContext -> m v) -> Maybe TypeContext -> m v
forall a b. (a -> b) -> a -> b
$ TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ComparisonArguments

typeCheckImpl
  :: forall inp . Typeable inp
  => TcInstrHandler
  -> [Un.ExpandedOp]
  -> HST inp
  -> TypeCheckInstr (SomeInstr inp)
typeCheckImpl :: TcInstrHandler
-> [ExpandedOp] -> HST inp -> TypeCheckInstr (SomeInstr inp)
typeCheckImpl tcInstr :: TcInstrHandler
tcInstr instrs :: [ExpandedOp]
instrs t :: HST inp
t@(HST inp
a :: HST a) =
  case [ExpandedOp]
instrs of
    Un.WithSrcEx _ (i :: ExpandedOp
i@(Un.WithSrcEx _ _)) : rs :: [ExpandedOp]
rs -> TcInstrHandler
-> [ExpandedOp] -> HST inp -> TypeCheckInstr (SomeInstr inp)
forall (inp :: [T]).
Typeable inp =>
TcInstrHandler
-> [ExpandedOp] -> HST inp -> TypeCheckInstr (SomeInstr inp)
typeCheckImpl TcInstrHandler
tcInstr (ExpandedOp
i ExpandedOp -> [ExpandedOp] -> [ExpandedOp]
forall a. a -> [a] -> [a]
: [ExpandedOp]
rs) HST inp
t
    Un.WithSrcEx cs :: InstrCallStack
cs (Un.PrimEx i :: ExpandedInstr
i) : rs :: [ExpandedOp]
rs -> Maybe InstrCallStack
-> ExpandedInstr -> [ExpandedOp] -> TypeCheckInstr (SomeInstr inp)
typeCheckPrim (InstrCallStack -> Maybe InstrCallStack
forall a. a -> Maybe a
Just InstrCallStack
cs) ExpandedInstr
i [ExpandedOp]
rs
    Un.WithSrcEx cs :: InstrCallStack
cs (Un.SeqEx sq :: [ExpandedOp]
sq) : rs :: [ExpandedOp]
rs -> Maybe InstrCallStack
-> [ExpandedOp] -> [ExpandedOp] -> TypeCheckInstr (SomeInstr inp)
typeCheckSeq (InstrCallStack -> Maybe InstrCallStack
forall a. a -> Maybe a
Just InstrCallStack
cs) [ExpandedOp]
sq [ExpandedOp]
rs
    Un.PrimEx i :: ExpandedInstr
i : rs :: [ExpandedOp]
rs                 -> Maybe InstrCallStack
-> ExpandedInstr -> [ExpandedOp] -> TypeCheckInstr (SomeInstr inp)
typeCheckPrim Maybe InstrCallStack
forall a. Maybe a
Nothing ExpandedInstr
i [ExpandedOp]
rs
    Un.SeqEx sq :: [ExpandedOp]
sq : rs :: [ExpandedOp]
rs                 -> Maybe InstrCallStack
-> [ExpandedOp] -> [ExpandedOp] -> TypeCheckInstr (SomeInstr inp)
typeCheckSeq Maybe InstrCallStack
forall a. Maybe a
Nothing [ExpandedOp]
sq [ExpandedOp]
rs
    []                               -> SomeInstr inp -> TypeCheckInstr (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> TypeCheckInstr (SomeInstr inp))
-> SomeInstr inp -> TypeCheckInstr (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
a HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ Instr inp inp
forall (s :: [T]). Instr s s
Nop Instr inp inp -> HST inp -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST inp
a
  where
    -- If we know source location from the untyped instruction, keep it in the typed one.
    typeCheckPrim :: Maybe InstrCallStack
-> ExpandedInstr -> [ExpandedOp] -> TypeCheckInstr (SomeInstr inp)
typeCheckPrim (Just cs :: InstrCallStack
cs) i :: ExpandedInstr
i [] = (InstrCallStack -> InstrCallStack)
-> TypeCheckInstr (SomeInstr inp) -> TypeCheckInstr (SomeInstr 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
cs) (TypeCheckInstr (SomeInstr inp) -> TypeCheckInstr (SomeInstr inp))
-> TypeCheckInstr (SomeInstr inp) -> TypeCheckInstr (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ (ExpandedInstr -> HST inp -> TypeCheckInstr (SomeInstr inp)
TcInstrHandler
tcInstr ExpandedInstr
i HST inp
t TypeCheckInstr (SomeInstr inp)
-> (SomeInstr inp -> SomeInstr inp)
-> TypeCheckInstr (SomeInstr inp)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> InstrCallStack -> SomeInstr inp -> SomeInstr inp
wrapWithLoc InstrCallStack
cs)
    typeCheckPrim (Just cs :: InstrCallStack
cs) i :: ExpandedInstr
i rs :: [ExpandedOp]
rs = (InstrCallStack -> InstrCallStack)
-> TypeCheckInstr (SomeInstr inp) -> TypeCheckInstr (SomeInstr 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
cs) (TypeCheckInstr (SomeInstr inp) -> TypeCheckInstr (SomeInstr inp))
-> TypeCheckInstr (SomeInstr inp) -> TypeCheckInstr (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ TypeCheckInstr (SomeInstr inp)
-> (forall (inp' :: [T]) (out :: [T]).
    Instr inp' out -> Instr inp' out)
-> [ExpandedOp]
-> TypeCheckInstr (SomeInstr inp)
typeCheckImplDo (ExpandedInstr -> HST inp -> TypeCheckInstr (SomeInstr inp)
TcInstrHandler
tcInstr ExpandedInstr
i HST inp
t TypeCheckInstr (SomeInstr inp)
-> (SomeInstr inp -> SomeInstr inp)
-> TypeCheckInstr (SomeInstr inp)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> InstrCallStack -> SomeInstr inp -> SomeInstr inp
wrapWithLoc InstrCallStack
cs) forall (inp' :: [T]) (out :: [T]). Instr inp' out -> Instr inp' out
forall a. a -> a
id [ExpandedOp]
rs
    typeCheckPrim Nothing i :: ExpandedInstr
i [] = ExpandedInstr -> HST inp -> TypeCheckInstr (SomeInstr inp)
TcInstrHandler
tcInstr ExpandedInstr
i HST inp
t
    typeCheckPrim Nothing i :: ExpandedInstr
i rs :: [ExpandedOp]
rs = TypeCheckInstr (SomeInstr inp)
-> (forall (inp' :: [T]) (out :: [T]).
    Instr inp' out -> Instr inp' out)
-> [ExpandedOp]
-> TypeCheckInstr (SomeInstr inp)
typeCheckImplDo (ExpandedInstr -> HST inp -> TypeCheckInstr (SomeInstr inp)
TcInstrHandler
tcInstr ExpandedInstr
i HST inp
t) forall (inp' :: [T]) (out :: [T]). Instr inp' out -> Instr inp' out
forall a. a -> a
id [ExpandedOp]
rs

    typeCheckSeq :: Maybe InstrCallStack
-> [ExpandedOp] -> [ExpandedOp] -> TypeCheckInstr (SomeInstr inp)
typeCheckSeq (Just cs :: InstrCallStack
cs) sq :: [ExpandedOp]
sq = (InstrCallStack -> InstrCallStack)
-> TypeCheckInstr (SomeInstr inp) -> TypeCheckInstr (SomeInstr 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
cs) (TypeCheckInstr (SomeInstr inp) -> TypeCheckInstr (SomeInstr inp))
-> ([ExpandedOp] -> TypeCheckInstr (SomeInstr inp))
-> [ExpandedOp]
-> TypeCheckInstr (SomeInstr inp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeCheckInstr (SomeInstr inp)
-> (forall (inp' :: [T]) (out :: [T]).
    Instr inp' out -> Instr inp' out)
-> [ExpandedOp]
-> TypeCheckInstr (SomeInstr inp)
typeCheckImplDo (TcInstrHandler
-> [ExpandedOp] -> HST inp -> TypeCheckInstr (SomeInstr inp)
forall (inp :: [T]).
Typeable inp =>
TcInstrHandler
-> [ExpandedOp] -> HST inp -> TypeCheckInstr (SomeInstr inp)
typeCheckImpl TcInstrHandler
tcInstr [ExpandedOp]
sq HST inp
t) forall (inp' :: [T]) (out :: [T]). Instr inp' out -> Instr inp' out
Nested
    typeCheckSeq Nothing sq :: [ExpandedOp]
sq = TypeCheckInstr (SomeInstr inp)
-> (forall (inp' :: [T]) (out :: [T]).
    Instr inp' out -> Instr inp' out)
-> [ExpandedOp]
-> TypeCheckInstr (SomeInstr inp)
typeCheckImplDo (TcInstrHandler
-> [ExpandedOp] -> HST inp -> TypeCheckInstr (SomeInstr inp)
forall (inp :: [T]).
Typeable inp =>
TcInstrHandler
-> [ExpandedOp] -> HST inp -> TypeCheckInstr (SomeInstr inp)
typeCheckImpl TcInstrHandler
tcInstr [ExpandedOp]
sq HST inp
t) forall (inp' :: [T]) (out :: [T]). Instr inp' out -> Instr inp' out
Nested

    wrapWithLoc :: InstrCallStack -> SomeInstr inp -> SomeInstr inp
    wrapWithLoc :: InstrCallStack -> SomeInstr inp -> SomeInstr inp
wrapWithLoc _ si :: SomeInstr inp
si@(_ :/ (WithLoc _ _) ::: _) = SomeInstr inp
si
    wrapWithLoc cs :: InstrCallStack
cs (inp :: HST inp
inp :/ instr :: Instr inp out
instr ::: out :: HST out
out) = HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ InstrCallStack -> Instr inp out -> Instr inp out
forall (a :: [T]) (b :: [T]).
InstrCallStack -> Instr a b -> Instr a b
WithLoc InstrCallStack
cs Instr inp out
instr Instr inp out -> HST out -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST out
out
    wrapWithLoc _ si :: SomeInstr inp
si = SomeInstr inp
si

    typeCheckImplDo
      :: TypeCheckInstr (SomeInstr inp)
      -> (forall inp' out . Instr inp' out -> Instr inp' out)
      -> [Un.ExpandedOp]
      -> TypeCheckInstr (SomeInstr inp)
    typeCheckImplDo :: TypeCheckInstr (SomeInstr inp)
-> (forall (inp' :: [T]) (out :: [T]).
    Instr inp' out -> Instr inp' out)
-> [ExpandedOp]
-> TypeCheckInstr (SomeInstr inp)
typeCheckImplDo f :: TypeCheckInstr (SomeInstr inp)
f wrap :: forall (inp' :: [T]) (out :: [T]). Instr inp' out -> Instr inp' out
wrap rs :: [ExpandedOp]
rs = do
      _ :/ pi' :: SomeInstrOut inp
pi' <- TypeCheckInstr (SomeInstr inp)
f
      case SomeInstrOut inp
pi' of
        p :: Instr inp out
p ::: b :: HST out
b -> do
          _ :/ qi :: SomeInstrOut out
qi <- TcInstrHandler
-> [ExpandedOp] -> HST out -> TypeCheckInstr (SomeInstr out)
forall (inp :: [T]).
Typeable inp =>
TcInstrHandler
-> [ExpandedOp] -> HST inp -> TypeCheckInstr (SomeInstr inp)
typeCheckImpl TcInstrHandler
tcInstr [ExpandedOp]
rs HST out
b
          case SomeInstrOut out
qi of
            q :: Instr out out
q ::: c :: HST out
c -> case Instr out out
q of
              Seq _ _ ->
                SomeInstr inp -> TypeCheckInstr (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> TypeCheckInstr (SomeInstr inp))
-> SomeInstr inp -> TypeCheckInstr (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
a 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 (HST out -> Instr inp out -> Instr inp out
forall (d :: [T]) (c :: [T]). HST d -> Instr c d -> Instr c d
wrapWithNotes HST out
b (Instr inp out -> Instr inp out
forall (inp' :: [T]) (out :: [T]). Instr inp' out -> Instr inp' out
wrap Instr inp out
p)) Instr out out
q Instr inp out -> HST out -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST out
c
              -- Wrap the RHS if it is a single instruction and not a
              -- sequence
              _ ->
                SomeInstr inp -> TypeCheckInstr (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> TypeCheckInstr (SomeInstr inp))
-> SomeInstr inp -> TypeCheckInstr (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
a 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 (HST out -> Instr inp out -> Instr inp out
forall (d :: [T]) (c :: [T]). HST d -> Instr c d -> Instr c d
wrapWithNotes HST out
b (Instr inp out -> Instr inp out
forall (inp' :: [T]) (out :: [T]). Instr inp' out -> Instr inp' out
wrap Instr inp out
p)) (HST out -> Instr out out -> Instr out out
forall (d :: [T]) (c :: [T]). HST d -> Instr c d -> Instr c d
wrapWithNotes HST out
c Instr out out
q) Instr inp out -> HST out -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST out
c
            AnyOutInstr q :: forall (out :: [T]). Instr out out
q ->
              SomeInstr inp -> TypeCheckInstr (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> TypeCheckInstr (SomeInstr inp))
-> SomeInstr inp -> TypeCheckInstr (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
a 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 (HST out -> Instr inp out -> Instr inp out
forall (d :: [T]) (c :: [T]). HST d -> Instr c d -> Instr c d
wrapWithNotes HST out
b (Instr inp out -> Instr inp out
forall (inp' :: [T]) (out :: [T]). Instr inp' out -> Instr inp' out
wrap Instr inp out
p)) Instr out out
forall (out :: [T]). Instr out out
q)

        AnyOutInstr instr :: forall (out :: [T]). Instr inp out
instr ->
          case [ExpandedOp]
rs of
            [] ->
              SomeInstr inp -> TypeCheckInstr (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> TypeCheckInstr (SomeInstr inp))
-> SomeInstr inp -> TypeCheckInstr (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
a 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
instr
            r :: ExpandedOp
r : rr :: [ExpandedOp]
rr ->
              TCError -> TypeCheckInstr (SomeInstr inp)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TypeCheckInstr (SomeInstr inp))
-> TCError -> TypeCheckInstr (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ InstrCallStack -> NonEmpty ExpandedOp -> TCError
TCUnreachableCode (ExpandedOp -> InstrCallStack
extractInstrPos ExpandedOp
r) (ExpandedOp
r ExpandedOp -> [ExpandedOp] -> NonEmpty ExpandedOp
forall a. a -> [a] -> NonEmpty a
:| [ExpandedOp]
rr)

    wrapWithNotes :: HST d -> Instr c d -> Instr c d
    wrapWithNotes :: HST d -> Instr c d -> Instr c d
wrapWithNotes h :: HST d
h ins :: Instr c d
ins = case HST d
h of
      -- do not wrap in notes if the notes are "star"
      ((n :: Notes x
n, _, _) ::& _) | Notes x -> Bool
forall (t :: T). SingI t => Notes t -> Bool
isStar Notes x
n -> Instr c d
ins
      ((n :: Notes x
n, _, _) ::& _) -> PackedNotes (x : xs) -> Instr c (x : xs) -> Instr c (x : xs)
forall (b :: [T]) (a :: [T]).
PackedNotes b -> Instr a b -> Instr a b
InstrWithNotes (Notes x -> PackedNotes (x : xs)
forall (a :: T) (s :: [T]).
SingI a =>
Notes a -> PackedNotes (a : s)
PackedNotes Notes x
n) Instr c d
Instr c (x : xs)
ins
      SNil -> Instr c d
ins

    extractInstrPos :: Un.ExpandedOp -> InstrCallStack
    extractInstrPos :: ExpandedOp -> InstrCallStack
extractInstrPos (Un.WithSrcEx cs :: InstrCallStack
cs _) = InstrCallStack
cs
    extractInstrPos _ = InstrCallStack
forall a. Default a => a
def

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

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

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

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

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

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

sliceImpl
  :: (SliceOp c, Typeable c, inp ~ ('TNat ': 'TNat ': c ': rs), Monad m)
  => HST inp
  -> Un.VarAnn
  -> m (SomeInstr inp)
sliceImpl :: HST inp -> VarAnn -> m (SomeInstr inp)
sliceImpl i :: HST inp
i@(_ ::& _ ::& (cn :: Notes x
cn, Dict, cvn :: VarAnn
cvn) ::& rs :: HST xs
rs) vn :: VarAnn
vn = do
  let vn' :: VarAnn
vn' = VarAnn
vn VarAnn -> VarAnn -> VarAnn
forall k (t :: k). Annotation t -> Annotation t -> Annotation t
`orAnn` VarAnn -> VarAnn -> VarAnn
deriveVN "slice" VarAnn
cvn
      rn :: Notes ('TOption x)
rn = TypeAnn -> Notes x -> Notes ('TOption x)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
forall a. Default a => a
def Notes x
cn
  SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ Instr ('TNat : 'TNat : x : xs) ('TOption x : xs)
forall (s :: T) (s :: [T]).
(SliceOp s, KnownT s) =>
Instr ('TNat : 'TNat : s : s) ('TOption s : s)
SLICE Instr ('TNat : 'TNat : x : xs) ('TOption x : xs)
-> HST ('TOption x : xs) -> SomeInstrOut ('TNat : 'TNat : x : xs)
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Notes ('TOption x)
rn, Dict (WellTyped ('TOption x))
forall (a :: Constraint). a => Dict a
Dict, VarAnn
vn') (Notes ('TOption x), Dict (WellTyped ('TOption x)), VarAnn)
-> HST xs -> HST ('TOption x : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs)

concatImpl'
  :: (ConcatOp c, WellTyped c, inp ~ ('TList c : rs), Monad m)
  => HST inp
  -> Un.VarAnn
  -> m (SomeInstr inp)
concatImpl' :: HST inp -> VarAnn -> m (SomeInstr inp)
concatImpl' i :: HST inp
i@((NTList _ n :: Notes t
n, Dict, _) ::& rs :: HST xs
rs) vn :: VarAnn
vn = do
  SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ Instr ('TList t : xs) (t : xs)
forall (s :: T) (s :: [T]).
ConcatOp s =>
Instr ('TList s : s) (s : s)
CONCAT' Instr ('TList t : xs) (t : xs)
-> HST (t : xs) -> SomeInstrOut ('TList t : xs)
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Notes t
n, Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict, VarAnn
vn) (Notes t, Dict (WellTyped t), VarAnn) -> HST xs -> HST (t : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs)

concatImpl
  :: ( ConcatOp c, inp ~ (c ': c ': rs)
     , WellTyped c
     , MonadReader InstrCallStack m
     , MonadError TCError m
     )
  => HST inp
  -> Un.VarAnn
  -> m (SomeInstr inp)
concatImpl :: HST inp -> VarAnn -> m (SomeInstr inp)
concatImpl i :: HST inp
i@((cn1 :: Notes x
cn1, _, _) ::& (cn2 :: Notes x
cn2, _, _) ::& rs :: HST xs
rs) vn :: VarAnn
vn = do
  Notes x
cn <- ExpandedInstr
-> HST inp
-> Maybe TypeContext
-> Either AnnConvergeError (Notes x)
-> m (Notes x)
forall (m :: * -> *) (ts :: [T]) a.
(MonadReader InstrCallStack m, MonadError TCError m,
 Typeable ts) =>
ExpandedInstr
-> HST ts -> Maybe TypeContext -> Either AnnConvergeError a -> m a
onTypeCheckInstrAnnErr (VarAnn -> ExpandedInstr
forall op. VarAnn -> InstrAbstract op
Un.CONCAT VarAnn
vn) HST inp
i (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ConcatArgument) (Notes x -> Notes x -> Either AnnConvergeError (Notes x)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes x
cn1 Notes x
Notes x
cn2)
  pure $ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ Instr (x : x : xs) (x : xs)
forall (c :: T) (s :: [T]). ConcatOp c => Instr (c : c : s) (c : s)
CONCAT Instr (x : x : xs) (x : xs)
-> HST (x : xs) -> SomeInstrOut (x : x : xs)
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Notes x
cn, Dict (WellTyped x)
forall (a :: Constraint). a => Dict a
Dict, VarAnn
vn) (Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs)

-- | Helper function to construct instructions for binary arithmetic
-- operations.
arithImpl
  :: forall aop inp m n s t.
     ( ArithOp aop n m
     , Typeable (ArithRes aop n m ': s)
     , WellTyped (ArithRes aop n m)
     , inp ~ (n ': m ': s)
     , MonadReader InstrCallStack t
     , MonadError TCError t
     )
  => Instr inp (ArithRes aop n m ': s)
  -> HST inp
  -> VarAnn
  -> Un.ExpandedInstr
  -> t (SomeInstr inp)
arithImpl :: Instr inp (ArithRes aop n m : s)
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl mkInstr :: Instr inp (ArithRes aop n m : s)
mkInstr i :: HST inp
i@((an :: Notes x
an, _, _) ::& (bn :: Notes x
bn, _, _) ::& rs :: HST xs
rs) vn :: VarAnn
vn uInstr :: ExpandedInstr
uInstr = do
  case Proxy aop
-> Notes x
-> Notes x
-> Either AnnConvergeError (Notes (ArithRes aop x x))
forall k (aop :: k) (n :: T) (m :: T) (proxy :: k -> *).
ArithOp aop n m =>
proxy aop
-> Notes n
-> Notes m
-> Either AnnConvergeError (Notes (ArithRes aop n m))
convergeArith (Proxy aop
forall k (t :: k). Proxy t
Proxy @aop) Notes x
an Notes x
bn of
    Right cn :: Notes (ArithRes aop x x)
cn ->
      SomeInstr inp -> t (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> t (SomeInstr inp))
-> SomeInstr inp -> t (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ Instr inp (ArithRes aop n m : s)
Instr inp (ArithRes aop n m : xs)
mkInstr Instr inp (ArithRes aop n m : xs)
-> HST (ArithRes aop n m : xs) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Notes (ArithRes aop n m)
Notes (ArithRes aop x x)
cn, Dict (WellTyped (ArithRes aop n m))
forall (a :: Constraint). a => Dict a
Dict, VarAnn
vn) (Notes (ArithRes aop n m), Dict (WellTyped (ArithRes aop n m)),
 VarAnn)
-> HST xs -> HST (ArithRes aop n m : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs)
    Left err :: AnnConvergeError
err -> do
      ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> t (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader InstrCallStack m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). Typeable ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TCTypeError -> t (SomeInstr inp))
-> TCTypeError -> t (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ AnnConvergeError -> TCTypeError
AnnError AnnConvergeError
err

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

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

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

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

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

-- | Helper function to construct instructions for binary arithmetic
-- operations.
unaryArithImpl
  :: ( Typeable (UnaryArithRes aop n ': s)
     , WellTyped (UnaryArithRes aop n)
     , inp ~ (n ': s)
     , Monad t
     )
  => Instr inp (UnaryArithRes aop n ': s)
  -> HST inp
  -> VarAnn
  -> t (SomeInstr inp)
unaryArithImpl :: Instr inp (UnaryArithRes aop n : s)
-> HST inp -> VarAnn -> t (SomeInstr inp)
unaryArithImpl mkInstr :: Instr inp (UnaryArithRes aop n : s)
mkInstr i :: HST inp
i@(_ ::& rs :: HST xs
rs) vn :: VarAnn
vn = do
  SomeInstr inp -> t (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> t (SomeInstr inp))
-> SomeInstr inp -> t (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ Instr inp (UnaryArithRes aop n : s)
Instr inp (UnaryArithRes aop n : xs)
mkInstr Instr inp (UnaryArithRes aop n : xs)
-> HST (UnaryArithRes aop n : xs) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Notes (UnaryArithRes aop n)
forall (t :: T). SingI t => Notes t
starNotes, Dict (WellTyped (UnaryArithRes aop n))
forall (a :: Constraint). a => Dict a
Dict, VarAnn
vn) (Notes (UnaryArithRes aop n),
 Dict (WellTyped (UnaryArithRes aop n)), VarAnn)
-> HST xs -> HST (UnaryArithRes aop n : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs)