-- 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
-- @SomeInstr@, wrap it in a @WellTypedSeq@.
workOnInstr
  :: U.ExpandedExtInstr
  -> TypeCheckInstr (SomeInstr s)
  -> TypeCheckInstrNoExcept (TypeCheckedSeq s)
workOnInstr :: forall (s :: [T]).
ExpandedExtInstr
-> TypeCheckInstr (SomeInstr s)
-> TypeCheckInstrNoExcept (TypeCheckedSeq s)
workOnInstr ExpandedExtInstr
ext = (TCError
 -> MultiReaderT
      '[TypeCheckInstrEnv, TypeCheckEnv, TypeCheckOptions]
      Identity
      (TypeCheckedSeq s))
-> (SomeInstr s
    -> MultiReaderT
         '[TypeCheckInstrEnv, TypeCheckEnv, TypeCheckOptions]
         Identity
         (TypeCheckedSeq s))
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv, TypeCheckOptions]
     (ExceptT TCError Identity)
     (SomeInstr s)
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv, TypeCheckOptions]
     Identity
     (TypeCheckedSeq s)
forall a b.
(TCError -> TypeCheckInstrNoExcept a)
-> (b -> TypeCheckInstrNoExcept a)
-> TypeCheckInstr b
-> TypeCheckInstrNoExcept a
tcEither
  (\TCError
err -> TypeCheckedSeq s
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq s
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
      (TypeCheckedSeq s))
-> TypeCheckedSeq s
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq s)
forall a b. (a -> b) -> a -> b
$ TCError -> [IllTypedInstr] -> TypeCheckedSeq s
forall (inp :: [T]).
TCError -> [IllTypedInstr] -> TypeCheckedSeq inp
IllTypedSeq TCError
err [ExpandedOp -> IllTypedInstr
NonTypedInstr (ExpandedOp -> IllTypedInstr) -> ExpandedOp -> IllTypedInstr
forall a b. (a -> b) -> a -> b
$ ExpandedInstr -> ExpandedOp
U.PrimEx (ExpandedInstr -> ExpandedOp) -> ExpandedInstr -> ExpandedOp
forall a b. (a -> b) -> a -> b
$ ExpandedExtInstr -> ExpandedInstr
forall op. ExtInstrAbstract op -> InstrAbstract op
U.EXT ExpandedExtInstr
ext])
  (TypeCheckedSeq s
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq s
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
      (TypeCheckedSeq s))
-> (SomeInstr s -> TypeCheckedSeq s)
-> SomeInstr s
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeInstr s -> TypeCheckedSeq s
forall (inp :: [T]). SomeInstr inp -> TypeCheckedSeq inp
WellTypedSeq)

typeCheckExt
  :: forall s. SingI s
  => TcInstrHandler
  -> U.ExpandedExtInstr
  -> HST s
  -> TypeCheckInstrNoExcept (TypeCheckedSeq s)
typeCheckExt :: forall (s :: [T]).
SingI s =>
TcInstrHandler
-> ExpandedExtInstr
-> HST s
-> TypeCheckInstrNoExcept (TypeCheckedSeq s)
typeCheckExt TcInstrHandler
tcInstr ExpandedExtInstr
ext HST s
hst = do
  ErrorSrcPos
instrPos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (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 ExpandedExtInstr
ext of
    U.STACKTYPE StackTypePattern
s -> ExpandedExtInstr
-> TypeCheckInstr (SomeInstr s)
-> TypeCheckInstrNoExcept (TypeCheckedSeq s)
forall (s :: [T]).
ExpandedExtInstr
-> TypeCheckInstr (SomeInstr s)
-> TypeCheckInstrNoExcept (TypeCheckedSeq s)
workOnInstr ExpandedExtInstr
ext (TypeCheckInstr (SomeInstr s)
 -> TypeCheckInstrNoExcept (TypeCheckedSeq s))
-> TypeCheckInstr (SomeInstr s)
-> TypeCheckInstrNoExcept (TypeCheckedSeq s)
forall a b. (a -> b) -> a -> b
$
      HST s
-> Either ExtError (SomeInstr s) -> TypeCheckInstr (SomeInstr s)
forall (s :: [T]) a.
SingI s =>
HST s -> Either ExtError a -> TypeCheckInstr a
liftExtError HST s
hst (Either ExtError (SomeInstr s) -> TypeCheckInstr (SomeInstr s))
-> Either ExtError (SomeInstr s) -> TypeCheckInstr (SomeInstr s)
forall a b. (a -> b) -> a -> b
$ StackTypePattern -> SomeInstr s
stackTypeSomeInstr StackTypePattern
s SomeInstr s
-> Either ExtError BoundVars -> Either ExtError (SomeInstr 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   -> ExpandedExtInstr
-> TypeCheckInstr (SomeInstr s)
-> TypeCheckInstrNoExcept (TypeCheckedSeq s)
forall (s :: [T]).
ExpandedExtInstr
-> TypeCheckInstr (SomeInstr s)
-> TypeCheckInstrNoExcept (TypeCheckedSeq s)
workOnInstr ExpandedExtInstr
ext (TypeCheckInstr (SomeInstr s)
 -> TypeCheckInstrNoExcept (TypeCheckedSeq s))
-> TypeCheckInstr (SomeInstr s)
-> TypeCheckInstrNoExcept (TypeCheckedSeq s)
forall a b. (a -> b) -> a -> b
$
      PrintComment -> TypeCheckInstr (PrintComment s)
verifyPrint PrintComment
pc ReaderT
  TypeCheckInstrEnv
  (ReaderT
     TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
  (PrintComment s)
-> (PrintComment s -> SomeInstr s)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (SomeInstr s)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \PrintComment s
tpc -> ExtInstr s -> SomeInstr s
toSomeInstr (PrintComment s -> ExtInstr s
forall (s :: [T]). PrintComment s -> ExtInstr s
T.PRINT PrintComment s
tpc)
    U.UTEST_ASSERT U.TestAssert{[ExpandedOp]
Text
PrintComment
tassInstrs :: forall op. TestAssert op -> [op]
tassComment :: forall op. TestAssert op -> PrintComment
tassName :: forall op. TestAssert op -> Text
tassInstrs :: [ExpandedOp]
tassComment :: PrintComment
tassName :: Text
..} -> do
      let cons :: [TypeCheckedOp] -> InstrAbstract TypeCheckedOp
cons = ExtInstrAbstract TypeCheckedOp -> InstrAbstract TypeCheckedOp
forall op. ExtInstrAbstract op -> InstrAbstract op
U.EXT (ExtInstrAbstract TypeCheckedOp -> InstrAbstract TypeCheckedOp)
-> ([TypeCheckedOp] -> ExtInstrAbstract TypeCheckedOp)
-> [TypeCheckedOp]
-> InstrAbstract TypeCheckedOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestAssert TypeCheckedOp -> ExtInstrAbstract TypeCheckedOp
forall op. TestAssert op -> ExtInstrAbstract op
U.UTEST_ASSERT (TestAssert TypeCheckedOp -> ExtInstrAbstract TypeCheckedOp)
-> ([TypeCheckedOp] -> TestAssert TypeCheckedOp)
-> [TypeCheckedOp]
-> ExtInstrAbstract TypeCheckedOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> PrintComment -> [TypeCheckedOp] -> TestAssert TypeCheckedOp
forall op. Text -> PrintComment -> [op] -> TestAssert op
U.TestAssert Text
tassName PrintComment
tassComment
      TypeCheckInstrNoExcept (TypeCheckedSeq s)
-> ([TypeCheckedOp] -> InstrAbstract TypeCheckedOp)
-> (SomeInstr s -> TypeCheckInstr (SomeInstr s))
-> TypeCheckInstrNoExcept (TypeCheckedSeq s)
forall (inp :: [T]) (inp' :: [T]).
TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> ([TypeCheckedOp] -> InstrAbstract TypeCheckedOp)
-> (SomeInstr inp -> TypeCheckInstr (SomeInstr inp'))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
preserving (TcInstrHandler
-> [ExpandedOp]
-> HST s
-> TypeCheckInstrNoExcept (TypeCheckedSeq s)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl TcInstrHandler
tcInstr [ExpandedOp]
tassInstrs HST s
hst) [TypeCheckedOp] -> InstrAbstract TypeCheckedOp
cons ((SomeInstr s -> TypeCheckInstr (SomeInstr s))
 -> TypeCheckInstrNoExcept (TypeCheckedSeq s))
-> (SomeInstr s -> TypeCheckInstr (SomeInstr s))
-> TypeCheckInstrNoExcept (TypeCheckedSeq s)
forall a b. (a -> b) -> a -> b
$ \(HST s
_ :/ SomeInstrOut s
si) -> case SomeInstrOut s
si of
        AnyOutInstr forall (out :: [T]). Instr s out
_ -> TCError
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (SomeInstr s)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (SomeInstr s))
-> TCError
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (SomeInstr s)
forall a b. (a -> b) -> a -> b
$ SomeHST -> ErrorSrcPos -> ExtError -> TCError
TCExtError (HST s -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST s
hst) ErrorSrcPos
instrPos (ExtError -> TCError) -> ExtError -> TCError
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 (x :~: 'TBool)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (x :~: 'TBool)
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either TCError (x :~: 'TBool)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (x :~: 'TBool))
-> Either TCError (x :~: 'TBool)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (x :~: 'TBool)
forall a b. (a -> b) -> a -> b
$ (TCTypeError -> TCError)
-> Either TCTypeError (x :~: 'TBool)
-> Either TCError (x :~: 'TBool)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first
            (TCError -> TCTypeError -> TCError
forall a b. a -> b -> a
const (TCError -> TCTypeError -> TCError)
-> TCError -> TCTypeError -> TCError
forall a b. (a -> b) -> a -> b
$ SomeHST -> ErrorSrcPos -> ExtError -> TCError
TCExtError (HST s -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST s
hst) ErrorSrcPos
instrPos (ExtError -> TCError) -> ExtError -> TCError
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 (PrintComment s)
verifyPrint PrintComment
tassComment
          SomeInstr s
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (SomeInstr s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr s
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (SomeInstr s))
-> (ExtInstr s -> SomeInstr s)
-> ExtInstr s
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (SomeInstr s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtInstr s -> SomeInstr s
toSomeInstr (ExtInstr s
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (SomeInstr s))
-> ExtInstr s
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (SomeInstr 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
        SomeInstrOut s
_ ->
          TCError
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (SomeInstr s)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (SomeInstr s))
-> TCError
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (SomeInstr s)
forall a b. (a -> b) -> a -> b
$ SomeHST -> ErrorSrcPos -> ExtError -> TCError
TCExtError (HST s -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST s
hst) ErrorSrcPos
instrPos (ExtError -> TCError) -> ExtError -> TCError
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 s
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq s
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
      (TypeCheckedSeq s))
-> TypeCheckedSeq s
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT TypeCheckEnv (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq s)
forall a b. (a -> b) -> a -> b
$ SomeInstr s -> TypeCheckedSeq s
forall (inp :: [T]). SomeInstr inp -> TypeCheckedSeq inp
WellTypedSeq (SomeInstr s -> TypeCheckedSeq s)
-> SomeInstr s -> TypeCheckedSeq s
forall a b. (a -> b) -> a -> b
$ ExtInstr s -> SomeInstr s
toSomeInstr (ExtInstr s -> SomeInstr s) -> ExtInstr s -> SomeInstr 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 (T.PrintComment s)
    verifyPrint :: PrintComment -> TypeCheckInstr (PrintComment s)
verifyPrint (U.PrintComment [Either Text StackRef]
pc) = do
      let checkStRef :: Either Text StackRef
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Either Text (StackRef s))
checkStRef (Left Text
txt)             = Either Text (StackRef s)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Either Text (StackRef s))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Text (StackRef s)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Either Text (StackRef s)))
-> Either Text (StackRef s)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError 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 (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (StackRef s)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Either Text (StackRef s))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural
-> HST s
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (StackRef s)
forall (m :: * -> *) (s :: [T]).
(MonadError TCError 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 (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     [Either Text (StackRef s)]
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (PrintComment s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Either Text StackRef
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Either Text (StackRef s)))
-> [Either Text StackRef]
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError 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 (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Either Text (StackRef s))
checkStRef [Either Text StackRef]
pc

    toSomeInstr :: ExtInstr s -> SomeInstr s
toSomeInstr ExtInstr s
ext' = HST s
hst HST s -> SomeInstrOut s -> SomeInstr s
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ ExtInstr s -> Instr s s
forall (inp :: [T]). ExtInstr inp -> Instr inp inp
T.Ext ExtInstr s
ext' Instr s s -> HST s -> SomeInstrOut s
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST s
hst
    stackTypeSomeInstr :: StackTypePattern -> SomeInstr s
stackTypeSomeInstr StackTypePattern
s = HST s
hst HST s -> SomeInstrOut s -> SomeInstr s
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr 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 -> SomeInstrOut s
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST s
hst

liftExtError :: SingI s => HST s -> Either ExtError a -> TypeCheckInstr a
liftExtError :: forall (s :: [T]) a.
SingI s =>
HST s -> Either ExtError a -> TypeCheckInstr a
liftExtError HST s
hst Either ExtError a
ei = do
  ErrorSrcPos
instrPos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError 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 a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     a
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either TCError a
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      a)
-> Either TCError a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     a
forall a b. (a -> b) -> a -> b
$ (ExtError -> TCError) -> Either ExtError a -> Either TCError a
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (SomeHST -> ErrorSrcPos -> ExtError -> TCError
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 m, MonadReader TypeCheckInstrEnv m, SingI s)
  => Natural -> HST s -> m (T.StackRef s)
createStackRef :: forall (m :: * -> *) (s :: [T]).
(MonadError TCError 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 -> m (StackRef s)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> m (StackRef s)) -> TCError -> m (StackRef s)
forall a b. (a -> b) -> a -> b
$
        SomeHST -> ErrorSrcPos -> ExtError -> TCError
TCExtError (HST s -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST s
hst) ErrorSrcPos
instrPos (ExtError -> TCError) -> ExtError -> TCError
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)