module Morley.Michelson.TypeCheck.Ext
( typeCheckExt
) where
import Control.Monad.Except (MonadError, liftEither, throwError)
import Data.Constraint (Dict(..))
import Data.Map.Lazy (insert, lookup)
import Data.Singletons (SingI, fromSing)
import Data.Typeable ((:~:)(..))
import Morley.Michelson.TypeCheck.Error
import Morley.Michelson.TypeCheck.Helpers
import Morley.Michelson.TypeCheck.TypeCheck
import Morley.Michelson.TypeCheck.TypeCheckedSeq (IllTypedInstr(..), TypeCheckedSeq(..))
import Morley.Michelson.TypeCheck.Types
import Morley.Michelson.Typed (Notes(..), notesT, withUType)
import Morley.Michelson.Typed qualified as T
import Morley.Michelson.Untyped (Ty, TyVar(..), Var)
import Morley.Michelson.Untyped qualified as U
import Morley.Util.MismatchError
import Morley.Util.PeanoNatural (PeanoNatural(..))
workOnInstr
:: IsInstrOp op
=> U.ExtInstrAbstract op
-> TypeCheckInstr op (SomeTcInstr s)
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op s)
workOnInstr :: forall op (s :: [T]).
IsInstrOp op =>
ExtInstrAbstract op
-> TypeCheckInstr op (SomeTcInstr s)
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op s)
workOnInstr ExtInstrAbstract op
ext = (TcError' op
-> MultiReaderT
'[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
Identity
(TypeCheckedSeq op s))
-> (SomeTcInstr s
-> MultiReaderT
'[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
Identity
(TypeCheckedSeq op s))
-> MultiReaderT
'[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
(ExceptT (TcError' op) Identity)
(SomeTcInstr s)
-> MultiReaderT
'[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
Identity
(TypeCheckedSeq op s)
forall op a b.
(TcError' op -> TypeCheckInstrNoExcept op a)
-> (b -> TypeCheckInstrNoExcept op a)
-> TypeCheckInstr op b
-> TypeCheckInstrNoExcept op a
tcEither
(\TcError' op
err -> TypeCheckedSeq op s
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq op s
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op s))
-> TypeCheckedSeq op s
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op s)
forall a b. (a -> b) -> a -> b
$ TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op s
forall op (inp :: [T]).
TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
IllTypedSeq TcError' op
err [op -> IllTypedInstr op
forall op. op -> IllTypedInstr op
NonTypedInstr (op -> IllTypedInstr op) -> op -> IllTypedInstr op
forall a b. (a -> b) -> a -> b
$ InstrAbstract op -> op
forall op. IsInstrOp op => InstrAbstract op -> op
liftInstr (InstrAbstract op -> op) -> InstrAbstract op -> op
forall a b. (a -> b) -> a -> b
$ ExtInstrAbstract op -> InstrAbstract op
forall op. ExtInstrAbstract op -> InstrAbstract op
U.EXT ExtInstrAbstract op
ext])
(TypeCheckedSeq op s
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq op s
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op s))
-> (SomeTcInstr s -> TypeCheckedSeq op s)
-> SomeTcInstr s
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeTcInstr s -> TypeCheckedSeq op s
forall op (inp :: [T]). SomeTcInstr inp -> TypeCheckedSeq op inp
WellTypedSeq)
typeCheckExt
:: forall s op.
(SingI s, IsInstrOp op)
=> TcInstrBase op
-> U.ExtInstrAbstract op
-> HST s
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op s)
typeCheckExt :: forall (s :: [T]) op.
(SingI s, IsInstrOp op) =>
TcInstrBase op
-> ExtInstrAbstract op
-> HST s
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op s)
typeCheckExt TcInstrBase op
tcOp ExtInstrAbstract op
ext HST s
hst = do
ErrorSrcPos
instrPos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
ErrorSrcPos
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos
case ExtInstrAbstract op
ext of
U.STACKTYPE StackTypePattern
s -> ExtInstrAbstract op
-> TypeCheckInstr op (SomeTcInstr s)
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op s)
forall op (s :: [T]).
IsInstrOp op =>
ExtInstrAbstract op
-> TypeCheckInstr op (SomeTcInstr s)
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op s)
workOnInstr ExtInstrAbstract op
ext (TypeCheckInstr op (SomeTcInstr s)
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op s))
-> TypeCheckInstr op (SomeTcInstr s)
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op s)
forall a b. (a -> b) -> a -> b
$
HST s
-> Either ExtError (SomeTcInstr s)
-> TypeCheckInstr op (SomeTcInstr s)
forall (s :: [T]) a op.
SingI s =>
HST s -> Either ExtError a -> TypeCheckInstr op a
liftExtError HST s
hst (Either ExtError (SomeTcInstr s)
-> TypeCheckInstr op (SomeTcInstr s))
-> Either ExtError (SomeTcInstr s)
-> TypeCheckInstr op (SomeTcInstr s)
forall a b. (a -> b) -> a -> b
$ StackTypePattern -> SomeTcInstr s
stackTypeSomeInstr StackTypePattern
s SomeTcInstr s
-> Either ExtError BoundVars -> Either ExtError (SomeTcInstr s)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ BoundVars -> StackTypePattern -> HST s -> Either ExtError BoundVars
forall (xs :: [T]).
SingI xs =>
BoundVars
-> StackTypePattern -> HST xs -> Either ExtError BoundVars
checkStackType BoundVars
noBoundVars StackTypePattern
s HST s
hst
U.UPRINT PrintComment
pc -> ExtInstrAbstract op
-> TypeCheckInstr op (SomeTcInstr s)
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op s)
forall op (s :: [T]).
IsInstrOp op =>
ExtInstrAbstract op
-> TypeCheckInstr op (SomeTcInstr s)
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op s)
workOnInstr ExtInstrAbstract op
ext (TypeCheckInstr op (SomeTcInstr s)
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op s))
-> TypeCheckInstr op (SomeTcInstr s)
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op s)
forall a b. (a -> b) -> a -> b
$
PrintComment -> TypeCheckInstr op (PrintComment s)
verifyPrint PrintComment
pc ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(PrintComment s)
-> (PrintComment s -> SomeTcInstr s)
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(SomeTcInstr s)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \PrintComment s
tpc -> ExtInstr s -> SomeTcInstr s
toSomeInstr (PrintComment s -> ExtInstr s
forall (s :: [T]). PrintComment s -> ExtInstr s
T.PRINT PrintComment s
tpc)
U.UTEST_ASSERT U.TestAssert{[op]
Text
PrintComment
tassInstrs :: forall op. TestAssert op -> [op]
tassComment :: forall op. TestAssert op -> PrintComment
tassName :: forall op. TestAssert op -> Text
tassInstrs :: [op]
tassComment :: PrintComment
tassName :: Text
..} -> do
let cons :: [TypeCheckedOp op] -> InstrAbstract (TypeCheckedOp op)
cons = ExtInstrAbstract (TypeCheckedOp op)
-> InstrAbstract (TypeCheckedOp op)
forall op. ExtInstrAbstract op -> InstrAbstract op
U.EXT (ExtInstrAbstract (TypeCheckedOp op)
-> InstrAbstract (TypeCheckedOp op))
-> ([TypeCheckedOp op] -> ExtInstrAbstract (TypeCheckedOp op))
-> [TypeCheckedOp op]
-> InstrAbstract (TypeCheckedOp op)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestAssert (TypeCheckedOp op)
-> ExtInstrAbstract (TypeCheckedOp op)
forall op. TestAssert op -> ExtInstrAbstract op
U.UTEST_ASSERT (TestAssert (TypeCheckedOp op)
-> ExtInstrAbstract (TypeCheckedOp op))
-> ([TypeCheckedOp op] -> TestAssert (TypeCheckedOp op))
-> [TypeCheckedOp op]
-> ExtInstrAbstract (TypeCheckedOp op)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text
-> PrintComment
-> [TypeCheckedOp op]
-> TestAssert (TypeCheckedOp op)
forall op. Text -> PrintComment -> [op] -> TestAssert op
U.TestAssert Text
tassName PrintComment
tassComment
TypeCheckInstrNoExcept op (TypeCheckedSeq op s)
-> ([TypeCheckedOp op] -> InstrAbstract (TypeCheckedOp op))
-> (SomeTcInstr s -> TypeCheckInstr op (SomeTcInstr s))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op s)
forall op (inp :: [T]) (inp' :: [T]).
TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
-> ([TypeCheckedOp op] -> TypeCheckedInstr op)
-> (SomeTcInstr inp -> TypeCheckInstr op (SomeTcInstr inp'))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
preserving (TcInstrBase op -> TcInstr op [op]
forall op. IsInstrOp op => TcInstrBase op -> TcInstr op [op]
typeCheckImpl TcInstrBase op
tcOp [op]
tassInstrs HST s
hst) [TypeCheckedOp op] -> InstrAbstract (TypeCheckedOp op)
cons ((SomeTcInstr s -> TypeCheckInstr op (SomeTcInstr s))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op s))
-> (SomeTcInstr s -> TypeCheckInstr op (SomeTcInstr s))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op s)
forall a b. (a -> b) -> a -> b
$ \(HST s
_ :/ SomeTcInstrOut s
si) -> case SomeTcInstrOut s
si of
AnyOutInstr forall (out :: [T]). Instr s out
_ -> TcError' op
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(SomeTcInstr s)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TcError' op
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(SomeTcInstr s))
-> TcError' op
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(SomeTcInstr s)
forall a b. (a -> b) -> a -> b
$ SomeHST -> ErrorSrcPos -> ExtError -> TcError' op
forall op. SomeHST -> ErrorSrcPos -> ExtError -> TcError' op
TcExtError (HST s -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST s
hst) ErrorSrcPos
instrPos (ExtError -> TcError' op) -> ExtError -> TcError' op
forall a b. (a -> b) -> a -> b
$ Text -> ExtError
TestAssertError
Text
"TEST_ASSERT has to return Bool, but it always fails"
Instr s out
instr ::: ((((SingT x, Dict (WellTyped x))
_ :: (T.SingT b, Dict (T.WellTyped b))) ::& HST xs
_)) -> do
x :~: 'TBool
Refl <- Either (TcError' op) (x :~: 'TBool)
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(x :~: 'TBool)
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either (TcError' op) (x :~: 'TBool)
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(x :~: 'TBool))
-> Either (TcError' op) (x :~: 'TBool)
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(x :~: 'TBool)
forall a b. (a -> b) -> a -> b
$ (TcTypeError -> TcError' op)
-> Either TcTypeError (x :~: 'TBool)
-> Either (TcError' op) (x :~: 'TBool)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first
(TcError' op -> TcTypeError -> TcError' op
forall a b. a -> b -> a
const (TcError' op -> TcTypeError -> TcError' op)
-> TcError' op -> TcTypeError -> TcError' op
forall a b. (a -> b) -> a -> b
$ SomeHST -> ErrorSrcPos -> ExtError -> TcError' op
forall op. SomeHST -> ErrorSrcPos -> ExtError -> TcError' op
TcExtError (HST s -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST s
hst) ErrorSrcPos
instrPos (ExtError -> TcError' op) -> ExtError -> TcError' op
forall a b. (a -> b) -> a -> b
$
Text -> ExtError
TestAssertError Text
"TEST_ASSERT has to return Bool, but returned something else")
(forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TcTypeError (a :~: b)
eqType @b @'T.TBool)
PrintComment s
tcom <- PrintComment -> TypeCheckInstr op (PrintComment s)
verifyPrint PrintComment
tassComment
SomeTcInstr s
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(SomeTcInstr s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeTcInstr s
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(SomeTcInstr s))
-> (ExtInstr s -> SomeTcInstr s)
-> ExtInstr s
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(SomeTcInstr s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtInstr s -> SomeTcInstr s
toSomeInstr (ExtInstr s
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(SomeTcInstr s))
-> ExtInstr s
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(SomeTcInstr s)
forall a b. (a -> b) -> a -> b
$ TestAssert s -> ExtInstr s
forall (s :: [T]). TestAssert s -> ExtInstr s
T.TEST_ASSERT (TestAssert s -> ExtInstr s) -> TestAssert s -> ExtInstr s
forall a b. (a -> b) -> a -> b
$ Text -> PrintComment s -> Instr s ('TBool : xs) -> TestAssert s
forall (s :: [T]) (out :: [T]).
Text -> PrintComment s -> Instr s ('TBool : out) -> TestAssert s
T.TestAssert Text
tassName PrintComment s
tcom Instr s out
Instr s ('TBool : xs)
instr
SomeTcInstrOut s
_ ->
TcError' op
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(SomeTcInstr s)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TcError' op
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(SomeTcInstr s))
-> TcError' op
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(SomeTcInstr s)
forall a b. (a -> b) -> a -> b
$ SomeHST -> ErrorSrcPos -> ExtError -> TcError' op
forall op. SomeHST -> ErrorSrcPos -> ExtError -> TcError' op
TcExtError (HST s -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST s
hst) ErrorSrcPos
instrPos (ExtError -> TcError' op) -> ExtError -> TcError' op
forall a b. (a -> b) -> a -> b
$
Text -> ExtError
TestAssertError Text
"TEST_ASSERT has to return Bool, but the stack is empty"
U.UCOMMENT Text
t ->
TypeCheckedSeq op s
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq op s
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op s))
-> TypeCheckedSeq op s
-> ReaderT
TypeCheckInstrEnv
(ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
(TypeCheckedSeq op s)
forall a b. (a -> b) -> a -> b
$ SomeTcInstr s -> TypeCheckedSeq op s
forall op (inp :: [T]). SomeTcInstr inp -> TypeCheckedSeq op inp
WellTypedSeq (SomeTcInstr s -> TypeCheckedSeq op s)
-> SomeTcInstr s -> TypeCheckedSeq op s
forall a b. (a -> b) -> a -> b
$ ExtInstr s -> SomeTcInstr s
toSomeInstr (ExtInstr s -> SomeTcInstr s) -> ExtInstr s -> SomeTcInstr s
forall a b. (a -> b) -> a -> b
$ CommentType -> ExtInstr s
forall (s :: [T]). CommentType -> ExtInstr s
T.COMMENT_ITEM (CommentType -> ExtInstr s) -> CommentType -> ExtInstr s
forall a b. (a -> b) -> a -> b
$ Text -> CommentType
T.JustComment Text
t
where
verifyPrint :: U.PrintComment -> TypeCheckInstr op (T.PrintComment s)
verifyPrint :: PrintComment -> TypeCheckInstr op (PrintComment s)
verifyPrint (U.PrintComment [Either Text StackRef]
pc) = do
let checkStRef :: Either Text StackRef
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(Either Text (StackRef s))
checkStRef (Left Text
txt) = Either Text (StackRef s)
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(Either Text (StackRef s))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Text (StackRef s)
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(Either Text (StackRef s)))
-> Either Text (StackRef s)
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(Either Text (StackRef s))
forall a b. (a -> b) -> a -> b
$ Text -> Either Text (StackRef s)
forall a b. a -> Either a b
Left Text
txt
checkStRef (Right (U.StackRef Natural
i)) = StackRef s -> Either Text (StackRef s)
forall a b. b -> Either a b
Right (StackRef s -> Either Text (StackRef s))
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(StackRef s)
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(Either Text (StackRef s))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural
-> HST s
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(StackRef s)
forall op (m :: * -> *) (s :: [T]).
(MonadError (TcError' op) m, MonadReader TypeCheckInstrEnv m,
SingI s) =>
Natural -> HST s -> m (StackRef s)
createStackRef Natural
i HST s
hst
[Either Text (StackRef s)] -> PrintComment s
forall (st :: [T]). [Either Text (StackRef st)] -> PrintComment st
T.PrintComment ([Either Text (StackRef s)] -> PrintComment s)
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
[Either Text (StackRef s)]
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(PrintComment s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Either Text StackRef
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(Either Text (StackRef s)))
-> [Either Text StackRef]
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
[Either Text (StackRef s)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Either Text StackRef
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
(Either Text (StackRef s))
checkStRef [Either Text StackRef]
pc
toSomeInstr :: ExtInstr s -> SomeTcInstr s
toSomeInstr ExtInstr s
ext' = HST s
hst HST s -> SomeTcInstrOut s -> SomeTcInstr s
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ ExtInstr s -> Instr s s
forall (inp :: [T]). ExtInstr inp -> Instr inp inp
T.Ext ExtInstr s
ext' Instr s s -> HST s -> SomeTcInstrOut s
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: HST s
hst
stackTypeSomeInstr :: StackTypePattern -> SomeTcInstr s
stackTypeSomeInstr StackTypePattern
s = HST s
hst HST s -> SomeTcInstrOut s -> SomeTcInstr s
forall (inp :: [T]).
HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp
:/ ExtInstr s -> Instr s s
forall (inp :: [T]). ExtInstr inp -> Instr inp inp
T.Ext (StackTypePattern -> ExtInstr s
forall (s :: [T]). StackTypePattern -> ExtInstr s
T.STACKTYPE StackTypePattern
s) Instr s s -> HST s -> SomeTcInstrOut s
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeTcInstrOut inp
::: HST s
hst
liftExtError :: SingI s => HST s -> Either ExtError a -> TypeCheckInstr op a
liftExtError :: forall (s :: [T]) a op.
SingI s =>
HST s -> Either ExtError a -> TypeCheckInstr op a
liftExtError HST s
hst Either ExtError a
ei = do
ErrorSrcPos
instrPos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
ErrorSrcPos
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos
Either (TcError' op) a
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
a
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either (TcError' op) a
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
a)
-> Either (TcError' op) a
-> ReaderT
TypeCheckInstrEnv
(ReaderT
(TypeCheckEnv op)
(ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
a
forall a b. (a -> b) -> a -> b
$ (ExtError -> TcError' op)
-> Either ExtError a -> Either (TcError' op) a
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (SomeHST -> ErrorSrcPos -> ExtError -> TcError' op
forall op. SomeHST -> ErrorSrcPos -> ExtError -> TcError' op
TcExtError (HST s -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST s
hst) ErrorSrcPos
instrPos) Either ExtError a
ei
checkStackType
:: SingI xs
=> BoundVars
-> U.StackTypePattern
-> HST xs
-> Either ExtError BoundVars
checkStackType :: forall (xs :: [T]).
SingI xs =>
BoundVars
-> StackTypePattern -> HST xs -> Either ExtError BoundVars
checkStackType (BoundVars Map Var Ty
vars Maybe SomeHST
boundStkRest) StackTypePattern
s HST xs
hst = Map Var Ty
-> Int -> StackTypePattern -> HST xs -> Either ExtError BoundVars
forall (xs :: [T]).
SingI xs =>
Map Var Ty
-> Int -> StackTypePattern -> HST xs -> Either ExtError BoundVars
go Map Var Ty
vars Int
0 StackTypePattern
s HST xs
hst
where
go :: SingI xs => Map Var Ty -> Int -> U.StackTypePattern -> HST xs
-> Either ExtError BoundVars
go :: forall (xs :: [T]).
SingI xs =>
Map Var Ty
-> Int -> StackTypePattern -> HST xs -> Either ExtError BoundVars
go Map Var Ty
m Int
_ StackTypePattern
U.StkRest HST xs
sr = case Maybe SomeHST
boundStkRest of
Maybe SomeHST
Nothing -> BoundVars -> Either ExtError BoundVars
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BoundVars -> Either ExtError BoundVars)
-> BoundVars -> Either ExtError BoundVars
forall a b. (a -> b) -> a -> b
$ Map Var Ty -> Maybe SomeHST -> BoundVars
BoundVars Map Var Ty
m (SomeHST -> Maybe SomeHST
forall a. a -> Maybe a
Just (SomeHST -> Maybe SomeHST) -> SomeHST -> Maybe SomeHST
forall a b. (a -> b) -> a -> b
$ HST xs -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST xs
sr)
Just si :: SomeHST
si@(SomeHST HST ts
sr') ->
(TcTypeError -> ExtError)
-> ((xs :~: ts) -> BoundVars)
-> Either TcTypeError (xs :~: ts)
-> Either ExtError BoundVars
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (StackTypePattern -> SomeHST -> SomeHST -> TcTypeError -> ExtError
StkRestMismatch StackTypePattern
s (HST xs -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST xs
sr) SomeHST
si)
(BoundVars -> (xs :~: ts) -> BoundVars
forall a b. a -> b -> a
const (BoundVars -> (xs :~: ts) -> BoundVars)
-> BoundVars -> (xs :~: ts) -> BoundVars
forall a b. (a -> b) -> a -> b
$ Map Var Ty -> Maybe SomeHST -> BoundVars
BoundVars Map Var Ty
m (SomeHST -> Maybe SomeHST
forall a. a -> Maybe a
Just SomeHST
si))
(HST xs -> HST ts -> Either TcTypeError (xs :~: ts)
forall (as :: [T]) (bs :: [T]).
(SingI as, SingI bs) =>
HST as -> HST bs -> Either TcTypeError (as :~: bs)
eqHST HST xs
sr HST ts
sr')
go Map Var Ty
m Int
_ StackTypePattern
U.StkEmpty HST xs
SNil = BoundVars -> Either ExtError BoundVars
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BoundVars -> Either ExtError BoundVars)
-> BoundVars -> Either ExtError BoundVars
forall a b. (a -> b) -> a -> b
$ Map Var Ty -> Maybe SomeHST -> BoundVars
BoundVars Map Var Ty
m Maybe SomeHST
forall a. Maybe a
Nothing
go Map Var Ty
_ Int
_ StackTypePattern
U.StkEmpty HST xs
_ = ExtError -> Either ExtError BoundVars
forall a b. a -> Either a b
Left (ExtError -> Either ExtError BoundVars)
-> ExtError -> Either ExtError BoundVars
forall a b. (a -> b) -> a -> b
$ StackTypePattern -> ExtError
LengthMismatch StackTypePattern
s
go Map Var Ty
_ Int
_ StackTypePattern
_ HST xs
SNil = ExtError -> Either ExtError BoundVars
forall a b. a -> Either a b
Left (ExtError -> Either ExtError BoundVars)
-> ExtError -> Either ExtError BoundVars
forall a b. (a -> b) -> a -> b
$ StackTypePattern -> ExtError
LengthMismatch StackTypePattern
s
go Map Var Ty
m Int
n (U.StkCons TyVar
tyVar StackTypePattern
ts) ((SingT x
xsing :: T.SingT xt, Dict (WellTyped x)
_) ::& HST xs
xs) =
let
handleType :: U.Ty -> Either ExtError BoundVars
handleType :: Ty -> Either ExtError BoundVars
handleType Ty
t =
Ty
-> (forall (t :: T).
SingI t =>
Notes t -> Either ExtError BoundVars)
-> Either ExtError BoundVars
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
t ((forall (t :: T). SingI t => Notes t -> Either ExtError BoundVars)
-> Either ExtError BoundVars)
-> (forall (t :: T).
SingI t =>
Notes t -> Either ExtError BoundVars)
-> Either ExtError BoundVars
forall a b. (a -> b) -> a -> b
$ \(Notes t
tann :: Notes t) -> do
x :~: t
Refl <- (TcTypeError -> ExtError)
-> Either TcTypeError (x :~: t) -> Either ExtError (x :~: t)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first
(\TcTypeError
_ -> StackTypePattern -> Int -> TcTypeError -> ExtError
TypeMismatch StackTypePattern
s Int
n (TcTypeError -> ExtError) -> TcTypeError -> ExtError
forall a b. (a -> b) -> a -> b
$ MismatchError T -> TcTypeError
TypeEqError MkMismatchError :: forall a. a -> a -> MismatchError a
MkMismatchError
{ meExpected :: T
meExpected = Sing x -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
SingT x
xsing, meActual :: T
meActual = Notes t -> T
forall (t :: T). Notes t -> T
notesT Notes t
tann })
(forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TcTypeError (a :~: b)
eqType @xt @t)
Map Var Ty
-> Int -> StackTypePattern -> HST xs -> Either ExtError BoundVars
forall (xs :: [T]).
SingI xs =>
Map Var Ty
-> Int -> StackTypePattern -> HST xs -> Either ExtError BoundVars
go Map Var Ty
m (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) StackTypePattern
ts HST xs
xs
in case TyVar
tyVar of
TyCon Ty
t -> Ty -> Either ExtError BoundVars
handleType Ty
t
VarID Var
v -> case Var -> Map Var Ty -> Maybe Ty
forall k a. Ord k => k -> Map k a -> Maybe a
lookup Var
v Map Var Ty
m of
Maybe Ty
Nothing -> let t :: Ty
t = T -> Ty
T.toUType (T -> Ty) -> T -> Ty
forall a b. (a -> b) -> a -> b
$ Sing x -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
SingT x
xsing in Map Var Ty
-> Int -> StackTypePattern -> HST xs -> Either ExtError BoundVars
forall (xs :: [T]).
SingI xs =>
Map Var Ty
-> Int -> StackTypePattern -> HST xs -> Either ExtError BoundVars
go (Var -> Ty -> Map Var Ty -> Map Var Ty
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert Var
v Ty
t Map Var Ty
m) (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) StackTypePattern
ts HST xs
xs
Just Ty
t -> Ty -> Either ExtError BoundVars
handleType Ty
t
createStackRef
:: (MonadError (TcError' op) m, MonadReader TypeCheckInstrEnv m, SingI s)
=> Natural -> HST s -> m (T.StackRef s)
createStackRef :: forall op (m :: * -> *) (s :: [T]).
(MonadError (TcError' op) m, MonadReader TypeCheckInstrEnv m,
SingI s) =>
Natural -> HST s -> m (StackRef s)
createStackRef Natural
idx HST s
hst =
case (HST s, Natural) -> Maybe (StackRef s)
forall (s :: [T]). (HST s, Natural) -> Maybe (StackRef s)
doCreate (HST s
hst, Natural
idx) of
Just StackRef s
sr -> StackRef s -> m (StackRef s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackRef s
sr
Maybe (StackRef s)
Nothing -> do
ErrorSrcPos
instrPos <- 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' op -> m (StackRef s)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TcError' op -> m (StackRef s)) -> TcError' op -> m (StackRef s)
forall a b. (a -> b) -> a -> b
$
SomeHST -> ErrorSrcPos -> ExtError -> TcError' op
forall op. SomeHST -> ErrorSrcPos -> ExtError -> TcError' op
TcExtError (HST s -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST s
hst) ErrorSrcPos
instrPos (ExtError -> TcError' op) -> ExtError -> TcError' op
forall a b. (a -> b) -> a -> b
$
StackRef -> StackSize -> ExtError
InvalidStackReference (Natural -> StackRef
U.StackRef Natural
idx) (Natural -> StackSize
StackSize (Natural -> StackSize) -> Natural -> StackSize
forall a b. (a -> b) -> a -> b
$ HST s -> Natural
forall (xs :: [T]). HST xs -> Natural
lengthHST HST s
hst)
where
doCreate :: forall s. (HST s, Natural) -> Maybe (T.StackRef s)
doCreate :: forall (s :: [T]). (HST s, Natural) -> Maybe (StackRef s)
doCreate = \case
(HST s
SNil, Natural
_) -> Maybe (StackRef s)
forall a. Maybe a
Nothing
(((SingT x, Dict (WellTyped x))
_ ::& HST xs
_), Natural
0) -> StackRef s -> Maybe (StackRef s)
forall a. a -> Maybe a
Just (PeanoNatural 'Z -> StackRef s
forall (st :: [T]) (idx :: Nat).
RequireLongerThan st idx =>
PeanoNatural idx -> StackRef st
T.StackRef PeanoNatural 'Z
forall (n :: Nat). (n ~ 'Z) => PeanoNatural n
Zero)
(((SingT x, Dict (WellTyped x))
_ ::& HST xs
st), Natural
i) -> do
T.StackRef PeanoNatural idx
ns <- (HST xs, Natural) -> Maybe (StackRef xs)
forall (s :: [T]). (HST s, Natural) -> Maybe (StackRef s)
doCreate (HST xs
st, Natural
i Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)
StackRef s -> Maybe (StackRef s)
forall (m :: * -> *) a. Monad m => a -> m a
return (StackRef s -> Maybe (StackRef s))
-> StackRef s -> Maybe (StackRef s)
forall a b. (a -> b) -> a -> b
$ PeanoNatural ('S idx) -> StackRef s
forall (st :: [T]) (idx :: Nat).
RequireLongerThan st idx =>
PeanoNatural idx -> StackRef st
T.StackRef (PeanoNatural idx -> PeanoNatural ('S idx)
forall (n :: Nat) (m :: Nat).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural idx
ns)