module Morley.Michelson.TypeCheck.Helpers
( hstToTs
, eqHST
, eqHST1
, lengthHST
, ensureDistinctAsc
, handleError
, eqType
, onTypeCheckInstrErr
, onScopeCheckInstrErr
, typeCheckInstrErr
, typeCheckInstrErr'
, typeCheckImpl
, typeCheckImplStripped
, memImpl
, getImpl
, updImpl
, getUpdImpl
, sliceImpl
, concatImpl
, concatImpl'
, sizeImpl
, arithImpl
, addImpl
, subImpl
, mulImpl
, edivImpl
, unaryArithImpl
, unaryArithImplAnnotated
, withCompareableCheck
) where
import Prelude hiding (EQ, GT, LT)
import Control.Monad.Except (MonadError, catchError, throwError)
import Data.Constraint (Dict(..), withDict)
import Data.Default (def)
import Data.Singletons (Sing, SingI(sing), demote, fromSing)
import Data.Singletons.Decide ((:~:)(Refl))
import Fmt (Buildable, (+|), (|+))
import Morley.Michelson.ErrorPos (ErrorSrcPos)
import Morley.Michelson.TypeCheck.Error (TCError(..), TCTypeError(..), TypeContext(..))
import Morley.Michelson.TypeCheck.TypeCheck
import Morley.Michelson.TypeCheck.TypeCheckedSeq (IllTypedInstr(..), TypeCheckedSeq(..))
import Morley.Michelson.TypeCheck.Types
import Morley.Michelson.Typed
(BadTypeForScope(..), CommentType(StackTypeComment), Comparable, ExtInstr(COMMENT_ITEM),
Instr(..), SingT(..), T(..), WellTyped, getComparableProofS, requireEq)
import Morley.Michelson.Typed.Annotation
import Morley.Michelson.Typed.Arith (Add, ArithOp(..), EDiv, Mul, Sub, UnaryArithOp(..))
import Morley.Michelson.Typed.Polymorphic
(ConcatOp, EDivOp(..), GetOp(..), MemOp(..), SizeOp, SliceOp, UpdOp(..))
import Morley.Michelson.Untyped qualified as Un
import Morley.Michelson.Untyped.Annotation (VarAnn)
import Morley.Util.MismatchError
import Morley.Util.Sing (eqI)
hstToTs :: HST st -> [T]
hstToTs :: forall (st :: [T]). HST st -> [T]
hstToTs = \case
HST st
SNil -> []
(SingT x
ts, Dict (WellTyped x)
_) ::& HST xs
hst -> Sing x -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
SingT x
ts T -> [T] -> [T]
forall a. a -> [a] -> [a]
: HST xs -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST xs
hst
eqHST
:: forall as bs. (SingI as, SingI bs)
=> HST as -> HST bs -> Either TCTypeError (as :~: bs)
eqHST :: forall (as :: [T]) (bs :: [T]).
(SingI as, SingI bs) =>
HST as -> HST bs -> Either TCTypeError (as :~: bs)
eqHST (HST as
hst :: HST xs) (HST bs
hst' :: HST ys) = do
case forall (a :: [T]) (b :: [T]).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @as @bs of
Maybe (as :~: bs)
Nothing -> TCTypeError -> Either TCTypeError (as :~: bs)
forall a b. a -> Either a b
Left (TCTypeError -> Either TCTypeError (as :~: bs))
-> TCTypeError -> Either TCTypeError (as :~: bs)
forall a b. (a -> b) -> a -> b
$ MismatchError [T] -> TCTypeError
StackEqError MkMismatchError :: forall a. a -> a -> MismatchError a
MkMismatchError {meActual :: [T]
meActual = HST as -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST as
hst, meExpected :: [T]
meExpected = HST bs -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST bs
hst'}
Just as :~: bs
Refl -> (as :~: as) -> Either TCTypeError (as :~: as)
forall a b. b -> Either a b
Right as :~: as
forall {k} (a :: k). a :~: a
Refl
eqHST1
:: forall t st. (SingI st, WellTyped t)
=> HST st -> Either TCTypeError (st :~: '[t])
eqHST1 :: forall (t :: T) (st :: [T]).
(SingI st, WellTyped t) =>
HST st -> Either TCTypeError (st :~: '[t])
eqHST1 HST st
hst = do
let hst' :: HST '[t]
hst' = forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @t Sing t -> HST '[] -> HST '[t]
forall (x :: T) (xs :: [T]).
(WellTyped x, SingI xs) =>
Sing x -> HST xs -> HST (x : xs)
-:& HST '[]
SNil
case forall (a :: [T]) (b :: [T]).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @'[t] @st of
Maybe ('[t] :~: st)
Nothing -> TCTypeError -> Either TCTypeError (st :~: '[t])
forall a b. a -> Either a b
Left (TCTypeError -> Either TCTypeError (st :~: '[t]))
-> TCTypeError -> Either TCTypeError (st :~: '[t])
forall a b. (a -> b) -> a -> b
$ MismatchError [T] -> TCTypeError
StackEqError MkMismatchError :: forall a. a -> a -> MismatchError a
MkMismatchError {meActual :: [T]
meActual = HST st -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST st
hst, meExpected :: [T]
meExpected = HST '[t] -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs HST '[t]
hst'}
Just '[t] :~: st
Refl -> (st :~: st) -> Either TCTypeError (st :~: st)
forall a b. b -> Either a b
Right st :~: st
forall {k} (a :: k). a :~: a
Refl
lengthHST :: HST xs -> Natural
lengthHST :: forall (xs :: [T]). HST xs -> Natural
lengthHST ((SingT x, Dict (WellTyped x))
_ ::& HST xs
xs) = Natural
1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ HST xs -> Natural
forall (xs :: [T]). HST xs -> Natural
lengthHST HST xs
xs
lengthHST HST xs
SNil = Natural
0
ensureDistinctAsc :: (Ord b, Buildable a) => (a -> b) -> [a] -> Either Text [a]
ensureDistinctAsc :: forall b a.
(Ord b, Buildable a) =>
(a -> b) -> [a] -> Either Text [a]
ensureDistinctAsc a -> b
toCmp = \case
(a
e1 : a
e2 : [a]
l) ->
if a -> b
toCmp a
e1 b -> b -> Bool
forall a. Ord a => a -> a -> Bool
< a -> b
toCmp a
e2
then (a
e1 a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> [a]) -> Either Text [a] -> Either Text [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> b) -> [a] -> Either Text [a]
forall b a.
(Ord b, Buildable a) =>
(a -> b) -> [a] -> Either Text [a]
ensureDistinctAsc a -> b
toCmp (a
e2 a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
l)
else Text -> Either Text [a]
forall a b. a -> Either a b
Left (Text -> Either Text [a]) -> Text -> Either Text [a]
forall a b. (a -> b) -> a -> b
$ Builder
"Entries are unordered (" Builder -> Builder -> Text
forall b. FromBuilder b => Builder -> Builder -> b
+| a
e1 a -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
" >= " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| a
e2 a -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
")"
[a]
l -> [a] -> Either Text [a]
forall a b. b -> Either a b
Right [a]
l
handleError :: MonadError e m => (e -> m a) -> m a -> m a
handleError :: forall e (m :: * -> *) a.
MonadError e m =>
(e -> m a) -> m a -> m a
handleError = (m a -> (e -> m a) -> m a) -> (e -> m a) -> m a -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip m a -> (e -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError
eqType
:: forall (a :: T) (b :: T). (Each '[SingI] [a, b])
=> Either TCTypeError (a :~: b)
eqType :: forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TCTypeError (a :~: b)
eqType =
forall (a :: T) (b :: T) (m :: * -> *).
(SingI a, SingI b, Monad m) =>
(forall x. MismatchError T -> m x) -> m (a :~: b)
requireEq @a @b ((forall x. MismatchError T -> Either TCTypeError x)
-> Either TCTypeError (a :~: b))
-> (forall x. MismatchError T -> Either TCTypeError x)
-> Either TCTypeError (a :~: b)
forall a b. (a -> b) -> a -> b
$ TCTypeError -> Either TCTypeError x
forall a b. a -> Either a b
Left (TCTypeError -> Either TCTypeError x)
-> (MismatchError T -> TCTypeError)
-> MismatchError T
-> Either TCTypeError x
forall a b c. SuperComposition a b c => a -> b -> c
... MismatchError T -> TCTypeError
TypeEqError
onTypeCheckInstrErr
:: (MonadReader TypeCheckInstrEnv m, MonadError TCError m)
=> Un.ExpandedInstr -> SomeHST -> Maybe TypeContext
-> Either TCTypeError a -> m a
onTypeCheckInstrErr :: forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr
-> SomeHST -> Maybe TypeContext -> Either TCTypeError a -> m a
onTypeCheckInstrErr ExpandedInstr
instr SomeHST
hst Maybe TypeContext
mContext Either TCTypeError a
ei = do
(TCTypeError -> m a) -> (a -> m a) -> Either TCTypeError a -> m a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
instr SomeHST
hst Maybe TypeContext
mContext) a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Either TCTypeError a
ei
onScopeCheckInstrErr
:: forall (t :: T) m a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m, SingI t)
=> Un.ExpandedInstr -> SomeHST -> Maybe TypeContext
-> Either BadTypeForScope a -> m a
onScopeCheckInstrErr :: forall (t :: T) (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m, SingI t) =>
ExpandedInstr
-> SomeHST -> Maybe TypeContext -> Either BadTypeForScope a -> m a
onScopeCheckInstrErr ExpandedInstr
instr SomeHST
hst Maybe TypeContext
mContext = \case
Right a
a -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
Left BadTypeForScope
e -> do
ErrorSrcPos
pos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos -> m ErrorSrcPos
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos
TCError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> m a) -> TCError -> m a
forall a b. (a -> b) -> a -> b
$ ExpandedInstr
-> SomeHST
-> ErrorSrcPos
-> Maybe TypeContext
-> Maybe TCTypeError
-> TCError
TCFailedOnInstr ExpandedInstr
instr SomeHST
hst ErrorSrcPos
pos Maybe TypeContext
mContext (Maybe TCTypeError -> TCError) -> Maybe TCTypeError -> TCError
forall a b. (a -> b) -> a -> b
$
TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ T -> BadTypeForScope -> TCTypeError
UnsupportedTypeForScope (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @t) BadTypeForScope
e
typeCheckInstrErr
:: (MonadReader TypeCheckInstrEnv m, MonadError TCError m)
=> Un.ExpandedInstr -> SomeHST -> Maybe TypeContext
-> m a
typeCheckInstrErr :: forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> m a
typeCheckInstrErr ExpandedInstr
instr SomeHST
hst Maybe TypeContext
mContext = do
ErrorSrcPos
pos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos -> m ErrorSrcPos
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos
TCError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> m a) -> TCError -> m a
forall a b. (a -> b) -> a -> b
$ ExpandedInstr
-> SomeHST
-> ErrorSrcPos
-> Maybe TypeContext
-> Maybe TCTypeError
-> TCError
TCFailedOnInstr ExpandedInstr
instr SomeHST
hst ErrorSrcPos
pos Maybe TypeContext
mContext Maybe TCTypeError
forall a. Maybe a
Nothing
typeCheckInstrErr'
:: (MonadReader TypeCheckInstrEnv m, MonadError TCError m)
=> Un.ExpandedInstr -> SomeHST -> Maybe TypeContext
-> TCTypeError -> m a
typeCheckInstrErr' :: forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
instr SomeHST
hst Maybe TypeContext
mContext TCTypeError
err = do
ErrorSrcPos
pos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos -> m ErrorSrcPos
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos
TCError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> m a) -> TCError -> m a
forall a b. (a -> b) -> a -> b
$ ExpandedInstr
-> SomeHST
-> ErrorSrcPos
-> Maybe TypeContext
-> Maybe TCTypeError
-> TCError
TCFailedOnInstr ExpandedInstr
instr SomeHST
hst ErrorSrcPos
pos Maybe TypeContext
mContext (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just TCTypeError
err)
withCompareableCheck
:: forall a m v ts. (SingI ts, MonadReader TypeCheckInstrEnv m, MonadError TCError m)
=> Sing a
-> Un.ExpandedInstr
-> HST ts
-> (Comparable a => v)
-> m v
withCompareableCheck :: forall (a :: T) (m :: * -> *) v (ts :: [T]).
(SingI ts, MonadReader TypeCheckInstrEnv m,
MonadError TCError m) =>
Sing a -> ExpandedInstr -> HST ts -> (Comparable a => v) -> m v
withCompareableCheck Sing a
sng ExpandedInstr
instr HST ts
i Comparable a => v
act = case Sing a -> Maybe (Dict (Comparable a))
forall (a :: T). Sing a -> Maybe (Dict (Comparable a))
getComparableProofS Sing a
sng of
Just d :: Dict (Comparable a)
d@Dict (Comparable a)
Dict -> v -> m v
forall (f :: * -> *) a. Applicative f => a -> f a
pure (v -> m v) -> v -> m v
forall a b. (a -> b) -> a -> b
$ Dict (Comparable a) -> (Comparable a => v) -> v
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict Dict (Comparable a)
d Comparable a => v
act
Maybe (Dict (Comparable a))
Nothing -> ExpandedInstr -> SomeHST -> Maybe TypeContext -> m v
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> m a
typeCheckInstrErr ExpandedInstr
instr (HST ts -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST ts
i) (Maybe TypeContext -> m v) -> Maybe TypeContext -> m v
forall a b. (a -> b) -> a -> b
$ TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ComparisonArguments
typeCheckOpImpl
:: forall inp. SingI inp
=> TcInstrHandler
-> Un.ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl :: forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op' HST inp
hst = case ExpandedOp
op' of
Un.WithSrcEx ErrorSrcPos
_ op :: ExpandedOp
op@Un.WithSrcEx{} -> TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op HST inp
hst
Un.WithSrcEx ErrorSrcPos
loc (Un.PrimEx ExpandedInstr
op) -> ErrorSrcPos
-> ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrimWithLoc ErrorSrcPos
loc ExpandedInstr
op
Un.WithSrcEx ErrorSrcPos
loc (Un.SeqEx [ExpandedOp]
sq) -> ErrorSrcPos
-> [ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeqWithLoc ErrorSrcPos
loc [ExpandedOp]
sq
Un.PrimEx ExpandedInstr
op -> ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrim ExpandedInstr
op
Un.SeqEx [ExpandedOp]
sq -> [ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeq [ExpandedOp]
sq
where
typeCheckPrimWithLoc :: ErrorSrcPos -> Un.ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrimWithLoc :: ErrorSrcPos
-> ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrimWithLoc ErrorSrcPos
loc ExpandedInstr
op = (TypeCheckInstrEnv -> TypeCheckInstrEnv)
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (ASetter TypeCheckInstrEnv TypeCheckInstrEnv ErrorSrcPos ErrorSrcPos
-> ErrorSrcPos -> TypeCheckInstrEnv -> TypeCheckInstrEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TypeCheckInstrEnv TypeCheckInstrEnv ErrorSrcPos ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos ErrorSrcPos
loc)
(ErrorSrcPos -> TypeCheckedSeq inp -> TypeCheckedSeq inp
forall (inp :: [T]).
ErrorSrcPos -> TypeCheckedSeq inp -> TypeCheckedSeq inp
wrapWithLoc ErrorSrcPos
loc (TypeCheckedSeq inp -> TypeCheckedSeq inp)
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrim ExpandedInstr
op)
typeCheckPrim :: Un.ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrim :: ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckPrim ExpandedInstr
op = ExpandedInstr
-> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
TcInstrHandler
tcInstr ExpandedInstr
op HST inp
hst
typeCheckSeqWithLoc :: ErrorSrcPos -> [Un.ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeqWithLoc :: ErrorSrcPos
-> [ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeqWithLoc ErrorSrcPos
loc = (TypeCheckedSeq inp -> TypeCheckedSeq inp)
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ErrorSrcPos -> TypeCheckedSeq inp -> TypeCheckedSeq inp
forall (inp :: [T]).
ErrorSrcPos -> TypeCheckedSeq inp -> TypeCheckedSeq inp
wrapWithLoc ErrorSrcPos
loc) (ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp))
-> ([ExpandedOp]
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp))
-> [ExpandedOp]
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeCheckInstrEnv -> TypeCheckInstrEnv)
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (ASetter TypeCheckInstrEnv TypeCheckInstrEnv ErrorSrcPos ErrorSrcPos
-> ErrorSrcPos -> TypeCheckInstrEnv -> TypeCheckInstrEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TypeCheckInstrEnv TypeCheckInstrEnv ErrorSrcPos ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos ErrorSrcPos
loc) (ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp))
-> ([ExpandedOp]
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp))
-> [ExpandedOp]
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ExpandedOp]
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
[ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeq
typeCheckSeq :: [Un.ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeq :: [ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckSeq [ExpandedOp]
sq = TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl TcInstrHandler
tcInstr [ExpandedOp]
sq HST inp
hst
ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
-> (TypeCheckedSeq inp -> TypeCheckedSeq inp)
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (SomeInstr inp -> SomeInstr inp)
-> TypeCheckedSeq inp -> TypeCheckedSeq inp
forall (inp :: [T]) (inp' :: [T]).
(SomeInstr inp -> SomeInstr inp')
-> TypeCheckedSeq inp -> TypeCheckedSeq inp'
mapSeq ((forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeInstr inp -> SomeInstr inp
forall (inp :: [T]).
(forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeInstr inp -> SomeInstr inp
mapSomeInstr forall (out :: [T]). Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
Nested)
typeCheckImplNoLastTypeComment
:: forall inp . SingI inp
=> TcInstrHandler
-> [Un.ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
TcInstrHandler
_ [] HST inp
inputStack
= TypeCheckedSeq inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> TypeCheckedSeq inp
forall (inp :: [T]). SomeInstr inp -> TypeCheckedSeq inp
WellTypedSeq (HST inp
inputStack HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop Instr inp inp -> HST inp -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST inp
inputStack))
typeCheckImplNoLastTypeComment TcInstrHandler
tcInstr [ExpandedOp
op] HST inp
inputStack = do
TcInstrHandler
-> ExpandedOp
-> HST inp
-> MultiReaderT
'[TypeCheckInstrEnv, TypeCheckEnv, TypeCheckOptions]
Identity
(TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op HST inp
inputStack
ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
-> (TypeCheckedSeq inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp))
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (SomeInstr inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(SomeInstr inp))
-> TypeCheckedSeq inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall (f :: * -> *) (inp :: [T]) (inp' :: [T]).
Applicative f =>
(SomeInstr inp -> f (SomeInstr inp'))
-> TypeCheckedSeq inp -> f (TypeCheckedSeq inp')
mapMSeq SomeInstr inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(SomeInstr inp)
forall (inp :: [T]).
SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp)
prependStackTypeComment
typeCheckImplNoLastTypeComment TcInstrHandler
tcInstr (ExpandedOp
op : [ExpandedOp]
ops) HST inp
inputStack = do
TypeCheckedSeq inp
done <- TcInstrHandler
-> ExpandedOp
-> HST inp
-> MultiReaderT
'[TypeCheckInstrEnv, TypeCheckEnv, TypeCheckOptions]
Identity
(TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op HST inp
inputStack
ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
-> (TypeCheckedSeq inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp))
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (SomeInstr inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(SomeInstr inp))
-> TypeCheckedSeq inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall (f :: * -> *) (inp :: [T]) (inp' :: [T]).
Applicative f =>
(SomeInstr inp -> f (SomeInstr inp'))
-> TypeCheckedSeq inp -> f (TypeCheckedSeq inp')
mapMSeq SomeInstr inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(SomeInstr inp)
forall (inp :: [T]).
SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp)
prependStackTypeComment
TcInstrHandler
-> TypeCheckedSeq inp
-> [ExpandedOp]
-> MultiReaderT
'[TypeCheckInstrEnv, TypeCheckEnv, TypeCheckOptions]
Identity
(TypeCheckedSeq inp)
forall (inp :: [T]).
TcInstrHandler
-> TypeCheckedSeq inp
-> [ExpandedOp]
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
continueTypeChecking TcInstrHandler
tcInstr TypeCheckedSeq inp
done [ExpandedOp]
ops
continueTypeChecking
:: forall inp. ()
=> TcInstrHandler
-> TypeCheckedSeq inp
-> [Un.ExpandedOp]
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
continueTypeChecking :: forall (inp :: [T]).
TcInstrHandler
-> TypeCheckedSeq inp
-> [ExpandedOp]
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
continueTypeChecking TcInstrHandler
tcInstr TypeCheckedSeq inp
done [ExpandedOp]
rest = case TypeCheckedSeq inp
done of
WellTypedSeq SomeInstr inp
instr -> SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
handleFirst SomeInstr inp
instr
MixedSeq SomeInstr inp
i TCError
e [IllTypedInstr]
left -> TypeCheckedSeq inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
forall (inp :: [T]).
SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
MixedSeq SomeInstr inp
i TCError
e ([IllTypedInstr]
left [IllTypedInstr] -> [IllTypedInstr] -> [IllTypedInstr]
forall a. Semigroup a => a -> a -> a
<> (ExpandedOp -> IllTypedInstr) -> [ExpandedOp] -> [IllTypedInstr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map ExpandedOp -> IllTypedInstr
NonTypedInstr [ExpandedOp]
rest))
IllTypedSeq TCError
e [IllTypedInstr]
left -> TypeCheckedSeq inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
forall (inp :: [T]).
TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
IllTypedSeq TCError
e ([IllTypedInstr]
left [IllTypedInstr] -> [IllTypedInstr] -> [IllTypedInstr]
forall a. Semigroup a => a -> a -> a
<> (ExpandedOp -> IllTypedInstr) -> [ExpandedOp] -> [IllTypedInstr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map ExpandedOp -> IllTypedInstr
NonTypedInstr [ExpandedOp]
rest))
where
handleFirst :: SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
handleFirst :: SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
handleFirst packedInstr :: SomeInstr inp
packedInstr@(HST inp
inputStack :/ SomeInstrOut inp
instrAndOutputStack) = do
case SomeInstrOut inp
instrAndOutputStack of
Instr inp out
instr ::: HST out
outputStack -> do
TypeCheckedSeq out
nextPiece <- TcInstrHandler
-> [ExpandedOp]
-> HST out
-> TypeCheckInstrNoExcept (TypeCheckedSeq out)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment TcInstrHandler
tcInstr [ExpandedOp]
rest HST out
outputStack
let combiner :: SomeInstr out -> SomeInstr inp
combiner = HST inp -> Instr inp out -> SomeInstr out -> SomeInstr inp
forall {inp :: [T]} {inp :: [T]}.
HST inp -> Instr inp inp -> SomeInstr inp -> SomeInstr inp
combine HST inp
inputStack Instr inp out
instr
TypeCheckedSeq inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure case TypeCheckedSeq out
nextPiece of
WellTypedSeq SomeInstr out
nextInstr -> SomeInstr inp -> TypeCheckedSeq inp
forall (inp :: [T]). SomeInstr inp -> TypeCheckedSeq inp
WellTypedSeq (SomeInstr out -> SomeInstr inp
combiner SomeInstr out
nextInstr)
MixedSeq SomeInstr out
nextInstr TCError
err [IllTypedInstr]
left -> SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
forall (inp :: [T]).
SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
MixedSeq (SomeInstr out -> SomeInstr inp
combiner SomeInstr out
nextInstr) TCError
err [IllTypedInstr]
left
IllTypedSeq TCError
err [IllTypedInstr]
left -> SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
forall (inp :: [T]).
SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
MixedSeq SomeInstr inp
packedInstr TCError
err [IllTypedInstr]
left
AnyOutInstr{} -> TypeCheckedSeq inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure case [ExpandedOp]
rest of
[] -> SomeInstr inp -> TypeCheckedSeq inp
forall (inp :: [T]). SomeInstr inp -> TypeCheckedSeq inp
WellTypedSeq SomeInstr inp
packedInstr
ExpandedOp
op : [ExpandedOp]
ops -> (SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
forall (inp :: [T]).
SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
MixedSeq
SomeInstr inp
packedInstr
(ErrorSrcPos -> NonEmpty ExpandedOp -> TCError
TCUnreachableCode (ExpandedOp -> ErrorSrcPos
extractOpPos ExpandedOp
op) (ExpandedOp
op ExpandedOp -> [ExpandedOp] -> NonEmpty ExpandedOp
forall a. a -> [a] -> NonEmpty a
:| [ExpandedOp]
ops))
((ExpandedOp -> IllTypedInstr) -> [ExpandedOp] -> [IllTypedInstr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map ExpandedOp -> IllTypedInstr
NonTypedInstr [ExpandedOp]
ops))
combine :: HST inp -> Instr inp inp -> SomeInstr inp -> SomeInstr inp
combine HST inp
inp Instr inp inp
Nop (HST inp
_ :/ SomeInstrOut inp
nextPart) = HST inp
HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ SomeInstrOut inp
nextPart
combine HST inp
inp Instr inp inp
i1 (HST inp
_ :/ SomeInstrOut inp
nextPart) = HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ (forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeInstrOut inp -> SomeInstrOut inp
forall (inp :: [T]) (inp' :: [T]).
(forall (out :: [T]). Instr inp out -> Instr inp' out)
-> SomeInstrOut inp -> SomeInstrOut inp'
mapSomeInstrOut (Instr inp inp -> Instr inp out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr inp inp
i1) SomeInstrOut inp
nextPart
extractOpPos :: Un.ExpandedOp -> ErrorSrcPos
extractOpPos :: ExpandedOp -> ErrorSrcPos
extractOpPos (Un.WithSrcEx ErrorSrcPos
loc ExpandedOp
_) = ErrorSrcPos
loc
extractOpPos ExpandedOp
_ = ErrorSrcPos
forall a. Default a => a
def
typeCheckImplStripped
:: forall inp . SingI inp
=> TcInstrHandler
-> [Un.ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplStripped :: forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplStripped TcInstrHandler
tcInstr [] HST inp
inp
= TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment TcInstrHandler
tcInstr [] HST inp
inp
typeCheckImplStripped TcInstrHandler
tcInstr (ExpandedOp
op : [ExpandedOp]
ops) HST inp
inp = do
TypeCheckedSeq inp
done <- TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> ExpandedOp
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckOpImpl TcInstrHandler
tcInstr ExpandedOp
op HST inp
inp
TcInstrHandler
-> TypeCheckedSeq inp
-> [ExpandedOp]
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
TcInstrHandler
-> TypeCheckedSeq inp
-> [ExpandedOp]
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
continueTypeChecking TcInstrHandler
tcInstr TypeCheckedSeq inp
done [ExpandedOp]
ops
typeCheckImpl
:: forall inp . SingI inp
=> TcInstrHandler
-> [Un.ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl :: forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl TcInstrHandler
tcInstr [ExpandedOp]
ops HST inp
inputStack = do
TypeCheckedSeq inp
tcSeq <- TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplNoLastTypeComment TcInstrHandler
tcInstr [ExpandedOp]
ops HST inp
inputStack
(SomeInstr inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(SomeInstr inp))
-> TypeCheckedSeq inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq inp)
forall (f :: * -> *) (inp :: [T]) (inp' :: [T]).
Applicative f =>
(SomeInstr inp -> f (SomeInstr inp'))
-> TypeCheckedSeq inp -> f (TypeCheckedSeq inp')
mapMSeq SomeInstr inp
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
(SomeInstr inp)
forall {f :: * -> *} {inp :: [T]}.
MultiReader
(MultiReaderDepth TypeCheckOptions (MultiReaderIso f))
TypeCheckOptions
f =>
SomeInstr inp -> f (SomeInstr inp)
appendTypeComment TypeCheckedSeq inp
tcSeq
where
appendTypeComment :: SomeInstr inp -> f (SomeInstr inp)
appendTypeComment packedI :: SomeInstr inp
packedI@(HST inp
inp :/ SomeInstrOut inp
iAndOut) = do
Bool
verbose <- (TypeCheckOptions -> Bool) -> f Bool
forall (m :: * -> *) r a (n :: Peano).
MultiReader n r m =>
(r -> a) -> m a
asks' TypeCheckOptions -> Bool
tcVerbose
pure case (Bool
verbose, SomeInstrOut inp
iAndOut) of
(Bool
True, Instr inp out
i ::: HST out
out) -> HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ Instr inp out -> Instr out out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr inp out
i (HST out -> Instr out out
forall (st :: [T]). HST st -> Instr st st
stackTypeComment HST out
out) Instr inp out -> HST out -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST out
out
(Bool
True, AnyOutInstr forall (out :: [T]). Instr inp out
i) -> HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ (forall (out :: [T]). Instr inp out) -> SomeInstrOut inp
forall (inp :: [T]).
(forall (out :: [T]). Instr inp out) -> SomeInstrOut inp
AnyOutInstr (Instr inp out -> Instr out out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr inp out
forall (out :: [T]). Instr inp out
i Instr out out
forall (inp :: [T]). Instr inp inp
noStackTypeComment)
(Bool, SomeInstrOut inp)
_ -> SomeInstr inp
packedI
prependStackTypeComment
:: SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp)
packedInstr :: SomeInstr inp
packedInstr@(HST inp
inp :/ SomeInstrOut inp
_) = do
Bool
verbose <- (TypeCheckOptions -> Bool)
-> ReaderT
TypeCheckInstrEnv
(ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
Bool
forall (m :: * -> *) r a (n :: Peano).
MultiReader n r m =>
(r -> a) -> m a
asks' TypeCheckOptions -> Bool
tcVerbose
pure if Bool
verbose Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
&& (Bool -> Bool
not (SomeInstr inp -> Bool
forall (inp :: [T]). SomeInstr inp -> Bool
isNop' SomeInstr inp
packedInstr))
then (forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeInstr inp -> SomeInstr inp
forall (inp :: [T]).
(forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeInstr inp -> SomeInstr inp
mapSomeInstr (Instr inp inp -> Instr inp out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq (HST inp -> Instr inp inp
forall (st :: [T]). HST st -> Instr st st
stackTypeComment HST inp
inp)) SomeInstr inp
packedInstr
else SomeInstr inp
packedInstr
isNop' :: SomeInstr inp -> Bool
isNop' :: forall (inp :: [T]). SomeInstr inp -> Bool
isNop' (HST inp
_ :/ Instr inp out
i ::: HST out
_) = Instr inp out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp out
i
isNop' (HST inp
_ :/ AnyOutInstr forall (out :: [T]). Instr inp out
i) = Instr inp Any -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp Any
forall (out :: [T]). Instr inp out
i
isNop :: Instr inp out -> Bool
isNop :: forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop (WithLoc ErrorSrcPos
_ Instr inp out
i) = Instr inp out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp out
i
isNop (FrameInstr Proxy s
_ Instr a b
i) = Instr a b -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr a b
i
isNop (Seq Instr inp b
i1 Instr b out
i2) = Instr inp b -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp b
i1 Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
&& Instr b out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr b out
i2
isNop (Nested Instr inp out
i) = Instr inp out -> Bool
forall (inp :: [T]) (out :: [T]). Instr inp out -> Bool
isNop Instr inp out
i
isNop Instr inp out
Nop = Bool
True
isNop (Ext ExtInstr inp
_) = Bool
True
isNop Instr inp out
_ = Bool
False
mapMSeq
:: Applicative f
=> (SomeInstr inp -> f (SomeInstr inp'))
-> TypeCheckedSeq inp
-> f (TypeCheckedSeq inp')
mapMSeq :: forall (f :: * -> *) (inp :: [T]) (inp' :: [T]).
Applicative f =>
(SomeInstr inp -> f (SomeInstr inp'))
-> TypeCheckedSeq inp -> f (TypeCheckedSeq inp')
mapMSeq SomeInstr inp -> f (SomeInstr inp')
f TypeCheckedSeq inp
v = case TypeCheckedSeq inp
v of
WellTypedSeq SomeInstr inp
instr -> SomeInstr inp -> f (SomeInstr inp')
f SomeInstr inp
instr f (SomeInstr inp')
-> (SomeInstr inp' -> TypeCheckedSeq inp')
-> f (TypeCheckedSeq inp')
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> SomeInstr inp' -> TypeCheckedSeq inp'
forall (inp :: [T]). SomeInstr inp -> TypeCheckedSeq inp
WellTypedSeq
MixedSeq SomeInstr inp
instr TCError
err [IllTypedInstr]
tail' -> SomeInstr inp -> f (SomeInstr inp')
f SomeInstr inp
instr f (SomeInstr inp')
-> (SomeInstr inp' -> TypeCheckedSeq inp')
-> f (TypeCheckedSeq inp')
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \SomeInstr inp'
instr' -> SomeInstr inp' -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp'
forall (inp :: [T]).
SomeInstr inp -> TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
MixedSeq SomeInstr inp'
instr' TCError
err [IllTypedInstr]
tail'
IllTypedSeq TCError
err [IllTypedInstr]
tail' -> TypeCheckedSeq inp' -> f (TypeCheckedSeq inp')
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq inp' -> f (TypeCheckedSeq inp'))
-> TypeCheckedSeq inp' -> f (TypeCheckedSeq inp')
forall a b. (a -> b) -> a -> b
$ TCError -> [IllTypedInstr] -> TypeCheckedSeq inp'
forall (inp :: [T]).
TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
IllTypedSeq TCError
err [IllTypedInstr]
tail'
mapSeq
:: (SomeInstr inp -> SomeInstr inp')
-> TypeCheckedSeq inp
-> TypeCheckedSeq inp'
mapSeq :: forall (inp :: [T]) (inp' :: [T]).
(SomeInstr inp -> SomeInstr inp')
-> TypeCheckedSeq inp -> TypeCheckedSeq inp'
mapSeq SomeInstr inp -> SomeInstr inp'
f = Identity (TypeCheckedSeq inp') -> TypeCheckedSeq inp'
forall a. Identity a -> a
runIdentity (Identity (TypeCheckedSeq inp') -> TypeCheckedSeq inp')
-> (TypeCheckedSeq inp -> Identity (TypeCheckedSeq inp'))
-> TypeCheckedSeq inp
-> TypeCheckedSeq inp'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SomeInstr inp -> Identity (SomeInstr inp'))
-> TypeCheckedSeq inp -> Identity (TypeCheckedSeq inp')
forall (f :: * -> *) (inp :: [T]) (inp' :: [T]).
Applicative f =>
(SomeInstr inp -> f (SomeInstr inp'))
-> TypeCheckedSeq inp -> f (TypeCheckedSeq inp')
mapMSeq (SomeInstr inp' -> Identity (SomeInstr inp')
forall a. a -> Identity a
Identity (SomeInstr inp' -> Identity (SomeInstr inp'))
-> (SomeInstr inp -> SomeInstr inp')
-> SomeInstr inp
-> Identity (SomeInstr inp')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeInstr inp -> SomeInstr inp'
f)
stackTypeComment :: HST st -> Instr st st
= ExtInstr st -> Instr st st
forall (inp :: [T]). ExtInstr inp -> Instr inp inp
Ext (ExtInstr st -> Instr st st)
-> (HST st -> ExtInstr st) -> HST st -> Instr st st
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommentType -> ExtInstr st
forall (s :: [T]). CommentType -> ExtInstr s
COMMENT_ITEM (CommentType -> ExtInstr st)
-> (HST st -> CommentType) -> HST st -> ExtInstr st
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe [T] -> CommentType
StackTypeComment (Maybe [T] -> CommentType)
-> (HST st -> Maybe [T]) -> HST st -> CommentType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [T] -> Maybe [T]
forall a. a -> Maybe a
Just ([T] -> Maybe [T]) -> (HST st -> [T]) -> HST st -> Maybe [T]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HST st -> [T]
forall (st :: [T]). HST st -> [T]
hstToTs
noStackTypeComment :: Instr st st
= ExtInstr st -> Instr st st
forall (inp :: [T]). ExtInstr inp -> Instr inp inp
Ext (CommentType -> ExtInstr st
forall (s :: [T]). CommentType -> ExtInstr s
COMMENT_ITEM (Maybe [T] -> CommentType
StackTypeComment Maybe [T]
forall a. Maybe a
Nothing))
wrapWithLoc :: ErrorSrcPos -> TypeCheckedSeq inp -> TypeCheckedSeq inp
wrapWithLoc :: forall (inp :: [T]).
ErrorSrcPos -> TypeCheckedSeq inp -> TypeCheckedSeq inp
wrapWithLoc ErrorSrcPos
loc = (SomeInstr inp -> SomeInstr inp)
-> TypeCheckedSeq inp -> TypeCheckedSeq inp
forall (inp :: [T]) (inp' :: [T]).
(SomeInstr inp -> SomeInstr inp')
-> TypeCheckedSeq inp -> TypeCheckedSeq inp'
mapSeq ((SomeInstr inp -> SomeInstr inp)
-> TypeCheckedSeq inp -> TypeCheckedSeq inp)
-> (SomeInstr inp -> SomeInstr inp)
-> TypeCheckedSeq inp
-> TypeCheckedSeq inp
forall a b. (a -> b) -> a -> b
$ \SomeInstr inp
someInstr -> case SomeInstr inp
someInstr of
(HST inp
_ :/ WithLoc{} ::: HST out
_) -> SomeInstr inp
someInstr
(HST inp
inp :/ Instr inp out
instr ::: HST out
out) -> HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ ErrorSrcPos -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
ErrorSrcPos -> Instr inp out -> Instr inp out
WithLoc ErrorSrcPos
loc Instr inp out
instr Instr inp out -> HST out -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST out
out
(HST inp
inp :/ AnyOutInstr forall (out :: [T]). Instr inp out
instr) -> HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ ((forall (out :: [T]). Instr inp out) -> SomeInstrOut inp
forall (inp :: [T]).
(forall (out :: [T]). Instr inp out) -> SomeInstrOut inp
AnyOutInstr ((forall (out :: [T]). Instr inp out) -> SomeInstrOut inp)
-> (forall (out :: [T]). Instr inp out) -> SomeInstrOut inp
forall a b. (a -> b) -> a -> b
$ ErrorSrcPos -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
ErrorSrcPos -> Instr inp out -> Instr inp out
WithLoc ErrorSrcPos
loc Instr inp out
forall (out :: [T]). Instr inp out
instr)
memImpl
:: forall c memKey rs inp m .
( MemOp c
, SingI (MemOpKey c)
, inp ~ (memKey : c : rs)
, SingI rs
, MonadReader TypeCheckInstrEnv m
, MonadError TCError m
)
=> HST inp
-> VarAnn
-> m (SomeInstr inp)
memImpl :: forall (c :: T) (memKey :: T) (rs :: [T]) (inp :: [T])
(m :: * -> *).
(MemOp c, SingI (MemOpKey c), inp ~ (memKey : c : rs), SingI rs,
MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
HST inp -> VarAnn -> m (SomeInstr inp)
memImpl inputHST :: HST inp
inputHST@((SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
_ ::& HST xs
hstTail) VarAnn
varAnn =
case forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @memKey @(MemOpKey c) of
Right memKey :~: MemOpKey c
Refl ->
SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
inputHST HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/
AnnVar -> Instr (MemOpKey c : c : xs) ('TBool : xs)
forall (c :: T) (s :: [T]).
MemOp c =>
AnnVar -> Instr (MemOpKey c : c : s) ('TBool : s)
AnnMEM (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
varAnn) Instr inp ('TBool : xs) -> HST ('TBool : xs) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((SingT 'TBool
forall {k} (a :: k). SingI a => Sing a
sing, Dict (WellTyped 'TBool)
forall (a :: Constraint). a => Dict a
Dict) (SingT 'TBool, Dict (WellTyped 'TBool))
-> HST xs -> HST ('TBool : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
hstTail)
Left TCTypeError
m ->
ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) TCTypeError
m
where
uInstr :: ExpandedInstr
uInstr = VarAnn -> ExpandedInstr
forall op. VarAnn -> InstrAbstract op
Un.MEM VarAnn
varAnn
getImpl
:: forall c getKey rs inp m .
( GetOp c, SingI (GetOpKey c)
, WellTyped (GetOpVal c)
, inp ~ (getKey : c : rs)
, SingI rs
, MonadReader TypeCheckInstrEnv m
, MonadError TCError m
)
=> HST inp
-> SingT (GetOpVal c)
-> VarAnn
-> m (SomeInstr inp)
getImpl :: forall (c :: T) (getKey :: T) (rs :: [T]) (inp :: [T])
(m :: * -> *).
(GetOp c, SingI (GetOpKey c), WellTyped (GetOpVal c),
inp ~ (getKey : c : rs), SingI rs, MonadReader TypeCheckInstrEnv m,
MonadError TCError m) =>
HST inp -> SingT (GetOpVal c) -> VarAnn -> m (SomeInstr inp)
getImpl inputHST :: HST inp
inputHST@((SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
_ ::& HST xs
hstTail) SingT (GetOpVal c)
valueSing VarAnn
varAnn =
case forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @getKey @(GetOpKey c) of
Right getKey :~: GetOpKey c
Refl ->
SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
inputHST HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/
AnnVar -> Instr (GetOpKey c : c : rs) ('TOption (GetOpVal c) : rs)
forall (c :: T) (s :: [T]).
(GetOp c, SingI (GetOpVal c)) =>
AnnVar -> Instr (GetOpKey c : c : s) ('TOption (GetOpVal c) : s)
AnnGET (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
varAnn) Instr inp ('TOption (GetOpVal c) : xs)
-> HST ('TOption (GetOpVal c) : xs) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Sing (GetOpVal c) -> SingT ('TOption (GetOpVal c))
forall (n :: T). Sing n -> SingT ('TOption n)
STOption Sing (GetOpVal c)
SingT (GetOpVal c)
valueSing, Dict (WellTyped ('TOption (GetOpVal c)))
forall (a :: Constraint). a => Dict a
Dict) (SingT ('TOption (GetOpVal c)),
Dict (WellTyped ('TOption (GetOpVal c))))
-> HST xs -> HST ('TOption (GetOpVal c) : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
hstTail)
Left TCTypeError
m ->
ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) TCTypeError
m
where
uInstr :: ExpandedInstr
uInstr = VarAnn -> ExpandedInstr
forall op. VarAnn -> InstrAbstract op
Un.GET VarAnn
varAnn
updImpl
:: forall c updKey updParams rs inp m .
( UpdOp c
, SingI (UpdOpKey c), SingI (UpdOpParams c)
, SingI rs
, inp ~ (updKey : updParams : c : rs)
, MonadReader TypeCheckInstrEnv m
, MonadError TCError m
)
=> HST inp
-> VarAnn
-> m (SomeInstr inp)
updImpl :: forall (c :: T) (updKey :: T) (updParams :: T) (rs :: [T])
(inp :: [T]) (m :: * -> *).
(UpdOp c, SingI (UpdOpKey c), SingI (UpdOpParams c), SingI rs,
inp ~ (updKey : updParams : c : rs),
MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
HST inp -> VarAnn -> m (SomeInstr inp)
updImpl inputHST :: HST inp
inputHST@((SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
cTuple ::& HST xs
hstTail) VarAnn
varAnn =
case (forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @updKey @(UpdOpKey c), forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @updParams @(UpdOpParams c)) of
(Right updKey :~: UpdOpKey c
Refl, Right updParams :~: UpdOpParams c
Refl) ->
SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
inputHST HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/
AnnVar -> Instr (UpdOpKey x : UpdOpParams x : x : xs) (x : xs)
forall (c :: T) (s :: [T]).
UpdOp c =>
AnnVar -> Instr (UpdOpKey c : UpdOpParams c : c : s) (c : s)
AnnUPDATE (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
varAnn) Instr inp (x : xs) -> HST (x : xs) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((SingT x, Dict (WellTyped x))
cTuple (SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
hstTail)
(Left TCTypeError
m, Either TCTypeError (updParams :~: UpdOpParams c)
_) ->
ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) TCTypeError
m
(Either TCTypeError (updKey :~: UpdOpKey c)
_, Left TCTypeError
m) ->
ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerValueType) TCTypeError
m
where
uInstr :: ExpandedInstr
uInstr = VarAnn -> ExpandedInstr
forall op. VarAnn -> InstrAbstract op
Un.UPDATE VarAnn
varAnn
getUpdImpl
:: forall c updKey updParams rs inp m .
( UpdOp c, GetOp c
, SingI (UpdOpKey c)
, SingI (GetOpVal c)
, inp ~ (updKey : updParams : c : rs)
, SingI rs
, GetOpKey c ~ UpdOpKey c
, UpdOpParams c ~ 'TOption (GetOpVal c)
, MonadReader TypeCheckInstrEnv m
, MonadError TCError m
)
=> HST inp
-> VarAnn
-> m (SomeInstr inp)
getUpdImpl :: forall (c :: T) (updKey :: T) (updParams :: T) (rs :: [T])
(inp :: [T]) (m :: * -> *).
(UpdOp c, GetOp c, SingI (UpdOpKey c), SingI (GetOpVal c),
inp ~ (updKey : updParams : c : rs), SingI rs,
GetOpKey c ~ UpdOpKey c, UpdOpParams c ~ 'TOption (GetOpVal c),
MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
HST inp -> VarAnn -> m (SomeInstr inp)
getUpdImpl inputHST :: HST inp
inputHST@((SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
hst1 ::& (SingT x, Dict (WellTyped x))
cTuple ::& HST xs
hstTail) VarAnn
varAnn =
case (forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @updKey @(UpdOpKey c), forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @updParams @(UpdOpParams c)) of
(Right updKey :~: UpdOpKey c
Refl, Right updParams :~: 'TOption (GetOpVal c)
Refl) ->
SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
inputHST HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/
AnnVar
-> Instr
(UpdOpKey c : UpdOpParams c : c : rs)
('TOption (GetOpVal c) : c : rs)
forall (c :: T) (s :: [T]).
(GetOp c, UpdOp c, SingI (GetOpVal c), UpdOpKey c ~ GetOpKey c) =>
AnnVar
-> Instr
(UpdOpKey c : UpdOpParams c : c : s)
('TOption (GetOpVal c) : c : s)
AnnGET_AND_UPDATE (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
varAnn) Instr inp (x : x : xs) -> HST (x : x : xs) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((SingT x, Dict (WellTyped x))
hst1 (SingT x, Dict (WellTyped x)) -> HST (x : xs) -> HST (x : x : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& (SingT x, Dict (WellTyped x))
cTuple (SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
hstTail)
(Left TCTypeError
m, Either TCTypeError (updParams :~: 'TOption (GetOpVal c))
_) ->
ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerKeyType) TCTypeError
m
(Either TCTypeError (updKey :~: UpdOpKey c)
_, Left TCTypeError
m) ->
ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
inputHST) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ContainerValueType) TCTypeError
m
where
uInstr :: ExpandedInstr
uInstr = VarAnn -> ExpandedInstr
forall op. VarAnn -> InstrAbstract op
Un.GET_AND_UPDATE VarAnn
varAnn
sizeImpl
:: (SizeOp c, inp ~ (c ': rs), Monad m)
=> HST inp
-> VarAnn
-> m (SomeInstr inp)
sizeImpl :: forall (c :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(SizeOp c, inp ~ (c : rs), Monad m) =>
HST inp -> VarAnn -> m (SomeInstr inp)
sizeImpl i :: HST inp
i@((SingT x, Dict (WellTyped x))
_ ::& HST xs
rs) VarAnn
vn =
SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ AnnVar -> Instr (c : xs) ('TNat : xs)
forall (c :: T) (s :: [T]).
SizeOp c =>
AnnVar -> Instr (c : s) ('TNat : s)
AnnSIZE (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
vn) Instr (c : xs) ('TNat : xs)
-> HST ('TNat : xs) -> SomeInstrOut (c : xs)
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((SingT 'TNat
forall {k} (a :: k). SingI a => Sing a
sing, Dict (WellTyped 'TNat)
forall (a :: Constraint). a => Dict a
Dict) (SingT 'TNat, Dict (WellTyped 'TNat)) -> HST xs -> HST ('TNat : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
rs)
sliceImpl
:: (SliceOp c, inp ~ ('TNat ': 'TNat ': c ': rs), Monad m)
=> HST inp
-> Un.VarAnn
-> m (SomeInstr inp)
sliceImpl :: forall (c :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(SliceOp c, inp ~ ('TNat : 'TNat : c : rs), Monad m) =>
HST inp -> VarAnn -> m (SomeInstr inp)
sliceImpl i :: HST inp
i@((SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
_ ::& (SingT x
cn, Dict (WellTyped x)
Dict) ::& HST xs
rs) VarAnn
vn = do
let rn :: SingT ('TOption c)
rn = Sing c -> SingT ('TOption c)
forall (n :: T). Sing n -> SingT ('TOption n)
STOption Sing c
SingT x
cn
SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ AnnVar -> Instr ('TNat : 'TNat : c : xs) ('TOption c : xs)
forall (c :: T) (s :: [T]).
(SliceOp c, SingI c) =>
AnnVar -> Instr ('TNat : 'TNat : c : s) ('TOption c : s)
AnnSLICE (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
vn) Instr ('TNat : 'TNat : c : xs) ('TOption c : xs)
-> HST ('TOption c : xs) -> SomeInstrOut ('TNat : 'TNat : c : xs)
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((SingT ('TOption c)
rn, Dict (WellTyped ('TOption c))
forall (a :: Constraint). a => Dict a
Dict) (SingT ('TOption c), Dict (WellTyped ('TOption c)))
-> HST xs -> HST ('TOption c : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
rs)
concatImpl'
:: (ConcatOp c, WellTyped c, inp ~ ('TList c : rs), Monad m)
=> HST inp
-> Un.VarAnn
-> m (SomeInstr inp)
concatImpl' :: forall (c :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(ConcatOp c, WellTyped c, inp ~ ('TList c : rs), Monad m) =>
HST inp -> VarAnn -> m (SomeInstr inp)
concatImpl' i :: HST inp
i@((STList Sing n
n, Dict (WellTyped x)
Dict) ::& HST xs
rs) VarAnn
vn = do
SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ AnnVar -> Instr ('TList c : xs) (c : xs)
forall (c :: T) (s :: [T]).
ConcatOp c =>
AnnVar -> Instr ('TList c : s) (c : s)
AnnCONCAT' (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
vn) Instr ('TList c : xs) (c : xs)
-> HST (c : xs) -> SomeInstrOut ('TList c : xs)
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((Sing n
SingT c
n, Dict (WellTyped c)
forall (a :: Constraint). a => Dict a
Dict) (SingT c, Dict (WellTyped c)) -> HST xs -> HST (c : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
rs)
concatImpl
:: ( ConcatOp c, inp ~ (c ': c ': rs)
, WellTyped c
, MonadReader TypeCheckInstrEnv m
)
=> HST inp
-> Un.VarAnn
-> m (SomeInstr inp)
concatImpl :: forall (c :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(ConcatOp c, inp ~ (c : c : rs), WellTyped c,
MonadReader TypeCheckInstrEnv m) =>
HST inp -> VarAnn -> m (SomeInstr inp)
concatImpl i :: HST inp
i@((SingT x
cn1, Dict (WellTyped x)
_) ::& (SingT x
_, Dict (WellTyped x)
_) ::& HST xs
rs) VarAnn
vn = do
SomeInstr inp -> m (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> m (SomeInstr inp))
-> SomeInstr inp -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ AnnVar -> Instr (x : x : xs) (x : xs)
forall (c :: T) (s :: [T]).
ConcatOp c =>
AnnVar -> Instr (c : c : s) (c : s)
AnnCONCAT (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
vn) Instr (x : x : xs) (x : xs)
-> HST (x : xs) -> SomeInstrOut (x : x : xs)
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((SingT x
cn1, Dict (WellTyped x)
forall (a :: Constraint). a => Dict a
Dict) (SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
rs)
arithImpl
:: forall aop inp m n s t.
( WellTyped (ArithRes aop n m)
, inp ~ (n ': m ': s)
, MonadReader TypeCheckInstrEnv t
)
=> (Anns '[VarAnn] -> Instr inp (ArithRes aop n m ': s))
-> HST inp
-> VarAnn
-> Un.ExpandedInstr
-> t (SomeInstr inp)
arithImpl :: forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl AnnVar -> Instr inp (ArithRes aop n m : s)
mkInstr i :: HST inp
i@((SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
_ ::& HST xs
rs) VarAnn
vn ExpandedInstr
_ =
SomeInstr inp -> t (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> t (SomeInstr inp))
-> SomeInstr inp -> t (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ AnnVar -> Instr inp (ArithRes aop n m : s)
mkInstr (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
vn) Instr inp (ArithRes aop n m : xs)
-> HST (ArithRes aop n m : xs) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((SingT (ArithRes aop n m)
forall {k} (a :: k). SingI a => Sing a
sing, Dict (WellTyped (ArithRes aop n m))
forall (a :: Constraint). a => Dict a
Dict) (SingT (ArithRes aop n m), Dict (WellTyped (ArithRes aop n m)))
-> HST xs -> HST (ArithRes aop n m : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
rs)
addImpl
:: forall a b inp rs m.
( Each '[SingI] [a, b]
, inp ~ (a ': b ': rs)
, SingI rs
, MonadReader TypeCheckInstrEnv m
, MonadError TCError m
)
=> Sing a -> Sing b
-> HST inp
-> VarAnn
-> Un.ExpandedInstr
-> m (SomeInstr inp)
addImpl :: forall (a :: T) (b :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(Each '[SingI] '[a, b], inp ~ (a : b : rs), SingI rs,
MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
Sing a
-> Sing b
-> HST inp
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr inp)
addImpl Sing a
t1 Sing b
t2 = case (Sing a
SingT a
t1, Sing b
SingT b
t2) of
(SingT a
STInt, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add AnnVar
-> Instr ('TInt : 'TInt : rs) (ArithRes Add 'TInt 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STInt, SingT b
STNat) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add AnnVar
-> Instr ('TInt : 'TNat : rs) (ArithRes Add 'TInt 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STNat, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add AnnVar
-> Instr ('TNat : 'TInt : rs) (ArithRes Add 'TNat 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STNat, SingT b
STNat) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add AnnVar
-> Instr ('TNat : 'TNat : rs) (ArithRes Add 'TNat 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STInt, SingT b
STTimestamp) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add AnnVar
-> Instr
('TInt : 'TTimestamp : rs) (ArithRes Add 'TInt 'TTimestamp : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STTimestamp, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add AnnVar
-> Instr
('TTimestamp : 'TInt : rs) (ArithRes Add 'TTimestamp 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STMutez, SingT b
STMutez) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add AnnVar
-> Instr
('TMutez : 'TMutez : rs) (ArithRes Add 'TMutez 'TMutez : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STBls12381Fr, SingT b
STBls12381Fr) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add AnnVar
-> Instr
('TBls12381Fr : 'TBls12381Fr : rs)
(ArithRes Add 'TBls12381Fr 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STBls12381G1, SingT b
STBls12381G1) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add AnnVar
-> Instr
('TBls12381G1 : 'TBls12381G1 : rs)
(ArithRes Add 'TBls12381G1 'TBls12381G1 : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a
STBls12381G2, SingT b
STBls12381G2) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Add AnnVar
-> Instr
('TBls12381G2 : 'TBls12381G2 : rs)
(ArithRes Add 'TBls12381G2 'TBls12381G2 : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
AnnVar -> Instr (n : m : s) (ArithRes Add n m : s)
AnnADD
(SingT a, SingT b)
_ -> \HST inp
i VarAnn
_ ExpandedInstr
uInstr -> ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TCTypeError -> m (SomeInstr inp))
-> TCTypeError -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$
T -> T -> TCTypeError
NotNumericTypes (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @a) (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @b)
edivImpl
:: forall a b inp rs m.
( SingI rs
, Each '[SingI] [a, b]
, inp ~ (a ': b ': rs)
, MonadReader TypeCheckInstrEnv m
, MonadError TCError m
)
=> Sing a -> Sing b
-> HST inp
-> VarAnn
-> Un.ExpandedInstr
-> m (SomeInstr inp)
edivImpl :: forall (a :: T) (b :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(SingI rs, Each '[SingI] '[a, b], inp ~ (a : b : rs),
MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
Sing a
-> Sing b
-> HST inp
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr inp)
edivImpl Sing a
t1 Sing b
t2 = case (Sing a
SingT a
t1, Sing b
SingT b
t2) of
(SingT a
STInt, SingT b
STInt) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(ArithOp EDiv n m,
ArithRes EDiv n m
~ 'TOption ('TPair (EDivOpRes n m) (EModOpRes n m)),
WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
inp ~ (n : m : s), MonadReader TypeCheckInstrEnv t) =>
HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
(SingT a
STInt, SingT b
STNat) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(ArithOp EDiv n m,
ArithRes EDiv n m
~ 'TOption ('TPair (EDivOpRes n m) (EModOpRes n m)),
WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
inp ~ (n : m : s), MonadReader TypeCheckInstrEnv t) =>
HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
(SingT a
STNat, SingT b
STInt) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(ArithOp EDiv n m,
ArithRes EDiv n m
~ 'TOption ('TPair (EDivOpRes n m) (EModOpRes n m)),
WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
inp ~ (n : m : s), MonadReader TypeCheckInstrEnv t) =>
HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
(SingT a
STNat, SingT b
STNat) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(ArithOp EDiv n m,
ArithRes EDiv n m
~ 'TOption ('TPair (EDivOpRes n m) (EModOpRes n m)),
WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
inp ~ (n : m : s), MonadReader TypeCheckInstrEnv t) =>
HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
(SingT a
STMutez, SingT b
STMutez) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(ArithOp EDiv n m,
ArithRes EDiv n m
~ 'TOption ('TPair (EDivOpRes n m) (EModOpRes n m)),
WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
inp ~ (n : m : s), MonadReader TypeCheckInstrEnv t) =>
HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
(SingT a
STMutez, SingT b
STNat) -> HST inp -> VarAnn -> ExpandedInstr -> m (SomeInstr inp)
forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(ArithOp EDiv n m,
ArithRes EDiv n m
~ 'TOption ('TPair (EDivOpRes n m) (EModOpRes n m)),
WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
inp ~ (n : m : s), MonadReader TypeCheckInstrEnv t) =>
HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo
(SingT a, SingT b)
_ -> \HST inp
i VarAnn
_ ExpandedInstr
uInstr -> ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TCTypeError -> m (SomeInstr inp))
-> TCTypeError -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$
T -> T -> TCTypeError
NotNumericTypes (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @a) (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @b)
edivImplDo
:: ( ArithOp EDiv n m
, ArithRes EDiv n m ~ 'TOption ('TPair (EDivOpRes n m) (EModOpRes n m))
, WellTyped (EModOpRes n m)
, WellTyped (EDivOpRes n m)
, inp ~ (n ': m ': s)
, MonadReader TypeCheckInstrEnv t
)
=> HST inp
-> VarAnn
-> Un.ExpandedInstr
-> t (SomeInstr inp)
edivImplDo :: forall (n :: T) (m :: T) (inp :: [T]) (s :: [T]) (t :: * -> *).
(ArithOp EDiv n m,
ArithRes EDiv n m
~ 'TOption ('TPair (EDivOpRes n m) (EModOpRes n m)),
WellTyped (EModOpRes n m), WellTyped (EDivOpRes n m),
inp ~ (n : m : s), MonadReader TypeCheckInstrEnv t) =>
HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
edivImplDo i :: HST inp
i@((SingT x, Dict (WellTyped x))
_ ::& (SingT x, Dict (WellTyped x))
_ ::& HST xs
rs) VarAnn
vn ExpandedInstr
_ =
SomeInstr inp -> t (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> t (SomeInstr inp))
-> SomeInstr inp -> t (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ AnnVar -> Instr (n : m : s) (ArithRes EDiv n m : s)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp EDiv n m =>
AnnVar -> Instr (n : m : s) (ArithRes EDiv n m : s)
AnnEDIV (VarAnn -> AnnVar
forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
Anns1 VarAnn
vn) Instr
(n : m : s)
('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : xs)
-> HST ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : xs)
-> SomeInstrOut (n : m : s)
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((SingT ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
forall {k} (a :: k). SingI a => Sing a
sing, Dict
(WellTyped ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m))))
forall (a :: Constraint). a => Dict a
Dict) (SingT ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m))),
Dict
(WellTyped ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))))
-> HST xs
-> HST ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
rs)
subImpl
:: forall a b inp rs m.
( Each '[SingI] [a, b]
, inp ~ (a ': b ': rs)
, SingI rs
, MonadReader TypeCheckInstrEnv m
, MonadError TCError m
)
=> Sing a -> Sing b
-> HST inp
-> VarAnn
-> Un.ExpandedInstr
-> m (SomeInstr inp)
subImpl :: forall (a :: T) (b :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(Each '[SingI] '[a, b], inp ~ (a : b : rs), SingI rs,
MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
Sing a
-> Sing b
-> HST inp
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr inp)
subImpl Sing a
t1 Sing b
t2 = case (Sing a
SingT a
t1, Sing b
SingT b
t2) of
(SingT a
STInt, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Sub AnnVar
-> Instr ('TInt : 'TInt : rs) (ArithRes Sub 'TInt 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Sub n m =>
AnnVar -> Instr (n : m : s) (ArithRes Sub n m : s)
AnnSUB
(SingT a
STInt, SingT b
STNat) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Sub AnnVar
-> Instr ('TInt : 'TNat : rs) (ArithRes Sub 'TInt 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Sub n m =>
AnnVar -> Instr (n : m : s) (ArithRes Sub n m : s)
AnnSUB
(SingT a
STNat, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Sub AnnVar
-> Instr ('TNat : 'TInt : rs) (ArithRes Sub 'TNat 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Sub n m =>
AnnVar -> Instr (n : m : s) (ArithRes Sub n m : s)
AnnSUB
(SingT a
STNat, SingT b
STNat) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Sub AnnVar
-> Instr ('TNat : 'TNat : rs) (ArithRes Sub 'TNat 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Sub n m =>
AnnVar -> Instr (n : m : s) (ArithRes Sub n m : s)
AnnSUB
(SingT a
STTimestamp, SingT b
STTimestamp) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Sub AnnVar
-> Instr
('TTimestamp : 'TTimestamp : rs)
(ArithRes Sub 'TTimestamp 'TTimestamp : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Sub n m =>
AnnVar -> Instr (n : m : s) (ArithRes Sub n m : s)
AnnSUB
(SingT a
STMutez, SingT b
STMutez) -> \HST inp
i VarAnn
_ ExpandedInstr
uInstr -> ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TCTypeError -> m (SomeInstr inp))
-> TCTypeError -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$
ExpandedInstr -> Text -> TCTypeError
InvalidInstruction ExpandedInstr
uInstr Text
"Use of SUB on `mutez` operands is deprecated; use SUB_MUTEZ"
(SingT a
STTimestamp, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Sub AnnVar
-> Instr
('TTimestamp : 'TInt : rs) (ArithRes Sub 'TTimestamp 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Sub n m =>
AnnVar -> Instr (n : m : s) (ArithRes Sub n m : s)
AnnSUB
(SingT a, SingT b)
_ -> \HST inp
i VarAnn
_ ExpandedInstr
uInstr -> ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TCTypeError -> m (SomeInstr inp))
-> TCTypeError -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$
T -> T -> TCTypeError
NotNumericTypes (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @a) (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @b)
mulImpl
:: forall a b inp rs m.
( Each '[SingI] [a, b]
, inp ~ (a ': b ': rs)
, SingI rs
, MonadReader TypeCheckInstrEnv m
, MonadError TCError m
)
=> Sing a -> Sing b
-> HST inp
-> VarAnn
-> Un.ExpandedInstr
-> m (SomeInstr inp)
mulImpl :: forall (a :: T) (b :: T) (inp :: [T]) (rs :: [T]) (m :: * -> *).
(Each '[SingI] '[a, b], inp ~ (a : b : rs), SingI rs,
MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
Sing a
-> Sing b
-> HST inp
-> VarAnn
-> ExpandedInstr
-> m (SomeInstr inp)
mulImpl Sing a
t1 Sing b
t2 = case (Sing a
SingT a
t1, Sing b
SingT b
t2) of
(SingT a
STInt, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul AnnVar
-> Instr ('TInt : 'TInt : rs) (ArithRes Mul 'TInt 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STInt, SingT b
STNat) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul AnnVar
-> Instr ('TInt : 'TNat : rs) (ArithRes Mul 'TInt 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STNat, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul AnnVar
-> Instr ('TNat : 'TInt : rs) (ArithRes Mul 'TNat 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STNat, SingT b
STNat) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul AnnVar
-> Instr ('TNat : 'TNat : rs) (ArithRes Mul 'TNat 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STNat, SingT b
STMutez) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul AnnVar
-> Instr ('TNat : 'TMutez : rs) (ArithRes Mul 'TNat 'TMutez : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STMutez, SingT b
STNat) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul AnnVar
-> Instr ('TMutez : 'TNat : rs) (ArithRes Mul 'TMutez 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STInt, SingT b
STBls12381Fr) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul AnnVar
-> Instr
('TInt : 'TBls12381Fr : rs) (ArithRes Mul 'TInt 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STNat, SingT b
STBls12381Fr) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul AnnVar
-> Instr
('TNat : 'TBls12381Fr : rs) (ArithRes Mul 'TNat 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STBls12381Fr, SingT b
STInt) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul AnnVar
-> Instr
('TBls12381Fr : 'TInt : rs) (ArithRes Mul 'TBls12381Fr 'TInt : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STBls12381Fr, SingT b
STNat) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul AnnVar
-> Instr
('TBls12381Fr : 'TNat : rs) (ArithRes Mul 'TBls12381Fr 'TNat : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STBls12381Fr, SingT b
STBls12381Fr) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul AnnVar
-> Instr
('TBls12381Fr : 'TBls12381Fr : rs)
(ArithRes Mul 'TBls12381Fr 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STBls12381G1, SingT b
STBls12381Fr) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul AnnVar
-> Instr
('TBls12381G1 : 'TBls12381Fr : rs)
(ArithRes Mul 'TBls12381G1 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a
STBls12381G2, SingT b
STBls12381Fr) -> forall {k} (aop :: k) (inp :: [T]) (m :: T) (n :: T) (s :: [T])
(t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
forall aop (inp :: [T]) (m :: T) (n :: T) (s :: [T]) (t :: * -> *).
(WellTyped (ArithRes aop n m), inp ~ (n : m : s),
MonadReader TypeCheckInstrEnv t) =>
(AnnVar -> Instr inp (ArithRes aop n m : s))
-> HST inp -> VarAnn -> ExpandedInstr -> t (SomeInstr inp)
arithImpl @Mul AnnVar
-> Instr
('TBls12381G2 : 'TBls12381Fr : rs)
(ArithRes Mul 'TBls12381G2 'TBls12381Fr : rs)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
AnnVar -> Instr (n : m : s) (ArithRes Mul n m : s)
AnnMUL
(SingT a, SingT b)
_ -> \HST inp
i VarAnn
_ ExpandedInstr
uInstr -> ExpandedInstr
-> SomeHST -> Maybe TypeContext -> TCTypeError -> m (SomeInstr inp)
forall (m :: * -> *) a.
(MonadReader TypeCheckInstrEnv m, MonadError TCError m) =>
ExpandedInstr -> SomeHST -> Maybe TypeContext -> TCTypeError -> m a
typeCheckInstrErr' ExpandedInstr
uInstr (HST inp -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST inp
i) (TypeContext -> Maybe TypeContext
forall a. a -> Maybe a
Just TypeContext
ArithmeticOperation) (TCTypeError -> m (SomeInstr inp))
-> TCTypeError -> m (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$
T -> T -> TCTypeError
NotNumericTypes (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @a) (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @b)
unaryArithImpl
:: ( WellTyped (UnaryArithRes aop n)
, inp ~ (n ': s)
, Monad t
)
=> Instr inp (UnaryArithRes aop n ': s)
-> HST inp
-> t (SomeInstr inp)
unaryArithImpl :: forall {k} (aop :: k) (n :: T) (inp :: [T]) (s :: [T])
(t :: * -> *).
(WellTyped (UnaryArithRes aop n), inp ~ (n : s), Monad t) =>
Instr inp (UnaryArithRes aop n : s) -> HST inp -> t (SomeInstr inp)
unaryArithImpl Instr inp (UnaryArithRes aop n : s)
mkInstr i :: HST inp
i@((SingT x, Dict (WellTyped x))
_ ::& HST xs
rs) = do
SomeInstr inp -> t (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> t (SomeInstr inp))
-> SomeInstr inp -> t (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ Instr inp (UnaryArithRes aop n : s)
Instr inp (UnaryArithRes aop n : xs)
mkInstr Instr inp (UnaryArithRes aop n : xs)
-> HST (UnaryArithRes aop n : xs) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((SingT (UnaryArithRes aop n)
forall {k} (a :: k). SingI a => Sing a
sing, Dict (WellTyped (UnaryArithRes aop n))
forall (a :: Constraint). a => Dict a
Dict) (SingT (UnaryArithRes aop n),
Dict (WellTyped (UnaryArithRes aop n)))
-> HST xs -> HST (UnaryArithRes aop n : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
rs)
unaryArithImplAnnotated
:: ( WellTyped (UnaryArithRes aop n)
, inp ~ (n ': s)
, Monad t
, n ~ UnaryArithRes aop n
)
=> Instr inp (UnaryArithRes aop n ': s)
-> HST inp
-> t (SomeInstr inp)
unaryArithImplAnnotated :: forall {k} (aop :: k) (n :: T) (inp :: [T]) (s :: [T])
(t :: * -> *).
(WellTyped (UnaryArithRes aop n), inp ~ (n : s), Monad t,
n ~ UnaryArithRes aop n) =>
Instr inp (UnaryArithRes aop n : s) -> HST inp -> t (SomeInstr inp)
unaryArithImplAnnotated Instr inp (UnaryArithRes aop n : s)
mkInstr i :: HST inp
i@((SingT x
n, Dict (WellTyped x)
_) ::& HST xs
rs) = do
SomeInstr inp -> t (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr inp -> t (SomeInstr inp))
-> SomeInstr inp -> t (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ HST inp
i HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ Instr inp (x : xs)
Instr inp (UnaryArithRes aop n : s)
mkInstr Instr inp (x : xs) -> HST (x : xs) -> SomeInstrOut inp
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: ((SingT x
n, Dict (WellTyped x)
forall (a :: Constraint). a => Dict a
Dict) (SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST xs
rs)