-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

-- | Type-checking of Morley extension.
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(..))

-- | Perform some, possibly throwing, action presumably making use of a supplied
-- external instruction. In case of an error, return @IllTypedSeq@ wrapping the
-- thrown error and the instruction. If the action successfully returns
-- @SomeTcInstr@, wrap it in a @WellTypedSeq@.
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

-- | Check that a @StackTypePattern@ matches the type of the current stack
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

-- | Create stack reference accessing element with a given index.
--
-- Fails when index is too large for the given stack.
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)