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

-- TODO [#712]: Remove this next major release
{-# OPTIONS_GHC -Wno-deprecations #-}

-- | Type-checking of Morley extension.
module Morley.Michelson.TypeCheck.Ext
  ( typeCheckExt
  ) where

import Control.Lens ((%=))
import Control.Monad.Except (MonadError, liftEither, throwError)
import Data.Constraint (Dict(..))
import Data.Map.Lazy (insert, lookup)
import Data.Singletons (SingI)
import Data.Typeable ((:~:)(..))

import Morley.Michelson.ErrorPos
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(..), converge, mkUType, notesT, withUType)
import Morley.Michelson.Typed qualified as T
import Morley.Michelson.Untyped
  (ExpandedOp, StackFn, Ty, TyVar(..), Var, VarAnn, sfnInPattern, sfnOutPattern, sfnQuantifiedVars,
  varSet)
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 :: ExpandedExtInstr
-> TypeCheckInstr (SomeInstr s)
-> TypeCheckInstrNoExcept (TypeCheckedSeq s)
workOnInstr ExpandedExtInstr
ext = (TCError -> TypeCheckInstrNoExcept (TypeCheckedSeq s))
-> (SomeInstr s -> TypeCheckInstrNoExcept (TypeCheckedSeq s))
-> TypeCheckInstr (SomeInstr s)
-> TypeCheckInstrNoExcept (TypeCheckedSeq s)
forall a b.
(TCError -> TypeCheckInstrNoExcept a)
-> (b -> TypeCheckInstrNoExcept a)
-> TypeCheckInstr b
-> TypeCheckInstrNoExcept a
tcEither
  (\TCError
err -> TypeCheckedSeq s -> TypeCheckInstrNoExcept (TypeCheckedSeq s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq s -> TypeCheckInstrNoExcept (TypeCheckedSeq s))
-> TypeCheckedSeq s -> TypeCheckInstrNoExcept (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 -> TypeCheckInstrNoExcept (TypeCheckedSeq s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq s -> TypeCheckInstrNoExcept (TypeCheckedSeq s))
-> (SomeInstr s -> TypeCheckedSeq s)
-> SomeInstr s
-> TypeCheckInstrNoExcept (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 :: TcInstrHandler
-> ExpandedExtInstr
-> HST s
-> TypeCheckInstrNoExcept (TypeCheckedSeq s)
typeCheckExt TcInstrHandler
tcInstr ExpandedExtInstr
ext HST s
hst = do
  InstrCallStack
instrPos <- ReaderT InstrCallStack TypeCheckNoExcept InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
  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.FN Text
t StackFn
sf [ExpandedOp]
op  -> TcInstrHandler
-> Text
-> StackFn
-> [ExpandedOp]
-> HST s
-> InstrCallStack
-> TypeCheckInstrNoExcept (TypeCheckedSeq s)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> Text
-> StackFn
-> [ExpandedOp]
-> HST inp
-> InstrCallStack
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
checkFn TcInstrHandler
tcInstr Text
t StackFn
sf [ExpandedOp]
op HST s
hst InstrCallStack
instrPos
    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 TypeCheckInstr (PrintComment s)
-> (PrintComment s -> SomeInstr s) -> TypeCheckInstr (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 -> TypeCheckInstr (SomeInstr s)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TypeCheckInstr (SomeInstr s))
-> TCError -> TypeCheckInstr (SomeInstr s)
forall a b. (a -> b) -> a -> b
$ SomeHST -> InstrCallStack -> ExtError -> TCError
TCExtError (HST s -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST s
hst) InstrCallStack
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 ::: ((((Notes x, Dict (WellTyped x), VarAnn)
_ :: (T.Notes b, Dict (T.WellTyped b), VarAnn)) ::& HST xs
_)) -> do
          x :~: 'TBool
Refl <- Either TCError (x :~: 'TBool)
-> ReaderT InstrCallStack TypeCheck (x :~: 'TBool)
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either TCError (x :~: 'TBool)
 -> ReaderT InstrCallStack TypeCheck (x :~: 'TBool))
-> Either TCError (x :~: 'TBool)
-> ReaderT InstrCallStack TypeCheck (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 -> InstrCallStack -> ExtError -> TCError
TCExtError (HST s -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST s
hst) InstrCallStack
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")
            (Each '[SingI] '[x, 'TBool] => Either TCTypeError (x :~: 'TBool)
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 -> TypeCheckInstr (SomeInstr s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr s -> TypeCheckInstr (SomeInstr s))
-> (ExtInstr s -> SomeInstr s)
-> ExtInstr s
-> TypeCheckInstr (SomeInstr s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtInstr s -> SomeInstr s
toSomeInstr (ExtInstr s -> TypeCheckInstr (SomeInstr s))
-> ExtInstr s -> TypeCheckInstr (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 (inp :: [T]) (out :: [T]).
Text
-> PrintComment inp -> Instr inp ('TBool : out) -> TestAssert inp
T.TestAssert Text
tassName PrintComment s
tcom Instr s out
Instr s ('TBool : xs)
instr
        SomeInstrOut s
_ ->
          TCError -> TypeCheckInstr (SomeInstr s)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TypeCheckInstr (SomeInstr s))
-> TCError -> TypeCheckInstr (SomeInstr s)
forall a b. (a -> b) -> a -> b
$ SomeHST -> InstrCallStack -> ExtError -> TCError
TCExtError (HST s -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST s
hst) InstrCallStack
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 ->
      -- TODO if we are going to analyze/parse programs from files,
      -- there should be parsing of string and creation of FunctionStarted/FunctionFinished/etc
      TypeCheckedSeq s -> TypeCheckInstrNoExcept (TypeCheckedSeq s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq s -> TypeCheckInstrNoExcept (TypeCheckedSeq s))
-> TypeCheckedSeq s -> TypeCheckInstrNoExcept (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 InstrCallStack TypeCheck (Either Text (StackRef s))
checkStRef (Left Text
txt)             = Either Text (StackRef s)
-> ReaderT InstrCallStack TypeCheck (Either Text (StackRef s))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Text (StackRef s)
 -> ReaderT InstrCallStack TypeCheck (Either Text (StackRef s)))
-> Either Text (StackRef s)
-> ReaderT InstrCallStack TypeCheck (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 InstrCallStack TypeCheck (StackRef s)
-> ReaderT InstrCallStack TypeCheck (Either Text (StackRef s))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural -> HST s -> ReaderT InstrCallStack TypeCheck (StackRef s)
forall (m :: * -> *) (s :: [T]).
(MonadError TCError m, MonadReader InstrCallStack 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 InstrCallStack TypeCheck [Either Text (StackRef s)]
-> TypeCheckInstr (PrintComment s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Either Text StackRef
 -> ReaderT InstrCallStack TypeCheck (Either Text (StackRef s)))
-> [Either Text StackRef]
-> ReaderT InstrCallStack TypeCheck [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 InstrCallStack TypeCheck (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 (s :: [T]). ExtInstr s -> Instr s s
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 (s :: [T]). ExtInstr s -> Instr s s
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 :: HST s -> Either ExtError a -> TypeCheckInstr a
liftExtError HST s
hst Either ExtError a
ei = do
  InstrCallStack
instrPos <- ReaderT InstrCallStack TypeCheck InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
  Either TCError a -> TypeCheckInstr a
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either TCError a -> TypeCheckInstr a)
-> Either TCError a -> TypeCheckInstr 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 -> InstrCallStack -> ExtError -> TCError
TCExtError (HST s -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST s
hst) InstrCallStack
instrPos) Either ExtError a
ei

-- | Check that the optional "forall" variables are consistent if present
checkVars :: Text -> StackFn -> Either ExtError ()
checkVars :: Text -> StackFn -> Either ExtError ()
checkVars Text
t StackFn
sf = case StackFn -> Maybe (Set Var)
sfnQuantifiedVars StackFn
sf of
  Just Set Var
qs
    | StackTypePattern -> Set Var
varSet (StackFn -> StackTypePattern
sfnInPattern StackFn
sf) Set Var -> Set Var -> Bool
forall a. Eq a => a -> a -> Bool
/= Set Var
qs -> ExtError -> Either ExtError ()
forall a b. a -> Either a b
Left (ExtError -> Either ExtError ()) -> ExtError -> Either ExtError ()
forall a b. (a -> b) -> a -> b
$ Text -> StackFn -> ExtError
VarError Text
t StackFn
sf
  Maybe (Set Var)
_ -> Either ExtError ()
forall (f :: * -> *). Applicative f => f ()
pass

-- | Executes function body, pushing @ExtFrame@ onto the state and checks
-- the pattern in @FN@.
checkFn
  :: SingI inp
  => TcInstrHandler
  -> Text
  -> StackFn
  -> [ExpandedOp]
  -> HST inp
  -> InstrCallStack
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
checkFn :: TcInstrHandler
-> Text
-> StackFn
-> [ExpandedOp]
-> HST inp
-> InstrCallStack
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
checkFn TcInstrHandler
tcInstr Text
t StackFn
sf [ExpandedOp]
body HST inp
inp InstrCallStack
loc = do
  ExpandedInstr
-> TypeCheckInstr BoundVars
-> (BoundVars -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall a (inp :: [T]).
ExpandedInstr
-> TypeCheckInstr a
-> (a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
guarding ([ExpandedOp] -> ExpandedInstr
forall op. [op] -> InstrAbstract op
con [ExpandedOp]
body) (HST inp -> TypeCheckInstr BoundVars
checkStart HST inp
inp) ((BoundVars -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
 -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> (BoundVars -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall a b. (a -> b) -> a -> b
$ \BoundVars
vars ->
    TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> ([TypeCheckedOp] -> InstrAbstract TypeCheckedOp)
-> (SomeInstr inp -> TypeCheckInstr (SomeInstr inp))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]) (inp' :: [T]).
TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> ([TypeCheckedOp] -> InstrAbstract TypeCheckedOp)
-> (SomeInstr inp -> TypeCheckInstr (SomeInstr inp'))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp')
preserving (TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImplStripped TcInstrHandler
tcInstr [ExpandedOp]
body HST inp
inp) [TypeCheckedOp] -> InstrAbstract TypeCheckedOp
forall op. [op] -> InstrAbstract op
con ((SomeInstr inp -> TypeCheckInstr (SomeInstr inp))
 -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> (SomeInstr inp -> TypeCheckInstr (SomeInstr inp))
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall a b. (a -> b) -> a -> b
$ \someI :: SomeInstr inp
someI@(HST inp
_ :/ SomeInstrOut inp
instrAndOut) ->
      case SomeInstrOut inp
instrAndOut of
        Instr inp out
_ ::: HST out
out -> BoundVars -> HST out -> TypeCheckInstr ()
forall (out :: [T]).
SingI out =>
BoundVars -> HST out -> TypeCheckInstr ()
checkEnd BoundVars
vars HST out
out TypeCheckInstr ()
-> SomeInstr inp -> TypeCheckInstr (SomeInstr inp)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> (forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeInstr inp -> SomeInstr inp
forall (inp :: [T]).
(forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeInstr inp -> SomeInstr inp
mapSomeInstr (InstrCallStack -> Instr inp out -> Instr inp out
forall (a :: [T]) (b :: [T]).
InstrCallStack -> Instr a b -> Instr a b
T.WithLoc InstrCallStack
loc (Instr inp out -> Instr inp out)
-> (Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> StackFn -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
Text -> StackFn -> Instr inp out -> Instr inp out
T.Fn Text
t StackFn
sf) SomeInstr inp
someI
        AnyOutInstr{} -> SomeInstr inp -> TypeCheckInstr (SomeInstr inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeInstr inp
someI
  where
    checkStart :: HST inp -> TypeCheckInstr BoundVars
checkStart HST inp
hst = do
      HST inp -> Either ExtError () -> TypeCheckInstr ()
forall (s :: [T]) a.
SingI s =>
HST s -> Either ExtError a -> TypeCheckInstr a
liftExtError HST inp
hst (Either ExtError () -> TypeCheckInstr ())
-> Either ExtError () -> TypeCheckInstr ()
forall a b. (a -> b) -> a -> b
$ Text -> StackFn -> Either ExtError ()
checkVars Text
t StackFn
sf
      BoundVars
vars <- HST inp -> Either ExtError BoundVars -> TypeCheckInstr BoundVars
forall (s :: [T]) a.
SingI s =>
HST s -> Either ExtError a -> TypeCheckInstr a
liftExtError HST inp
hst (Either ExtError BoundVars -> TypeCheckInstr BoundVars)
-> Either ExtError BoundVars -> TypeCheckInstr BoundVars
forall a b. (a -> b) -> a -> b
$ BoundVars
-> StackTypePattern -> HST inp -> Either ExtError BoundVars
forall (xs :: [T]).
SingI xs =>
BoundVars
-> StackTypePattern -> HST xs -> Either ExtError BoundVars
checkStackType BoundVars
noBoundVars (StackFn -> StackTypePattern
sfnInPattern StackFn
sf) HST inp
hst
      (TcExtFrames -> Identity TcExtFrames)
-> TypeCheckEnv -> Identity TypeCheckEnv
Lens' TypeCheckEnv TcExtFrames
tcExtFramesL ((TcExtFrames -> Identity TcExtFrames)
 -> TypeCheckEnv -> Identity TypeCheckEnv)
-> (TcExtFrames -> TcExtFrames) -> TypeCheckInstr ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (BoundVars
vars BoundVars -> TcExtFrames -> TcExtFrames
forall a. a -> [a] -> [a]
:)
      return BoundVars
vars

    checkEnd :: SingI out => BoundVars -> HST out -> TypeCheckInstr ()
    checkEnd :: BoundVars -> HST out -> TypeCheckInstr ()
checkEnd BoundVars
vars HST out
out = HST out -> Either ExtError () -> TypeCheckInstr ()
forall (s :: [T]) a.
SingI s =>
HST s -> Either ExtError a -> TypeCheckInstr a
liftExtError HST out
out (Either ExtError () -> TypeCheckInstr ())
-> Either ExtError () -> TypeCheckInstr ()
forall a b. (a -> b) -> a -> b
$
      Either ExtError BoundVars -> Either ExtError ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Either ExtError BoundVars -> Either ExtError ())
-> Either ExtError BoundVars -> Either ExtError ()
forall a b. (a -> b) -> a -> b
$ BoundVars
-> StackTypePattern -> HST out -> Either ExtError BoundVars
forall (xs :: [T]).
SingI xs =>
BoundVars
-> StackTypePattern -> HST xs -> Either ExtError BoundVars
checkStackType BoundVars
vars (StackFn -> StackTypePattern
sfnOutPattern StackFn
sf) HST out
out

    con :: [op] -> U.InstrAbstract op
    con :: [op] -> InstrAbstract op
con = ExtInstrAbstract op -> InstrAbstract op
forall op. ExtInstrAbstract op -> InstrAbstract op
U.EXT (ExtInstrAbstract op -> InstrAbstract op)
-> ([op] -> ExtInstrAbstract op) -> [op] -> InstrAbstract op
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> StackFn -> [op] -> ExtInstrAbstract op
forall op. Text -> StackFn -> [op] -> ExtInstrAbstract op
U.FN Text
t StackFn
sf

-- | Check that a @StackTypePattern@ matches the type of the current stack
checkStackType
  :: SingI xs
  => BoundVars
  -> U.StackTypePattern
  -> HST xs
  -> Either ExtError BoundVars
checkStackType :: 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 :: 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) ((Notes x
xann :: Notes xt, Dict (WellTyped x)
_, VarAnn
_) ::& 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 = Notes x -> T
forall (t :: T). Notes t -> T
notesT Notes x
xann, meActual :: T
meActual = Notes t -> T
forall (t :: T). Notes t -> T
notesT Notes t
tann })
              (Each '[SingI] '[x, t] => Either TCTypeError (x :~: t)
forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @xt @t)
            Either ExtError (Notes t) -> Either ExtError ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Either ExtError (Notes t) -> Either ExtError ())
-> Either ExtError (Notes t) -> Either ExtError ()
forall a b. (a -> b) -> a -> b
$ (AnnConvergeError -> ExtError)
-> Either AnnConvergeError (Notes t) -> Either ExtError (Notes t)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (StackTypePattern -> Int -> TCTypeError -> ExtError
TypeMismatch StackTypePattern
s Int
n (TCTypeError -> ExtError)
-> (AnnConvergeError -> TCTypeError)
-> AnnConvergeError
-> ExtError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnnConvergeError -> TCTypeError
AnnError) (Notes t -> Notes t -> Either AnnConvergeError (Notes t)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes t
tann Notes x
Notes t
xann)
            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 = Notes x -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes x
xann 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 InstrCallStack m, SingI s)
  => Natural -> HST s -> m (T.StackRef s)
createStackRef :: 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
      InstrCallStack
instrPos <- m InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
      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 -> InstrCallStack -> ExtError -> TCError
TCExtError (HST s -> SomeHST
forall (ts :: [T]). SingI ts => HST ts -> SomeHST
SomeHST HST s
hst) InstrCallStack
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 :: (HST s, Natural) -> Maybe (StackRef s)
doCreate = \case
      (HST s
SNil, Natural
_) -> Maybe (StackRef s)
forall a. Maybe a
Nothing
      (((Notes x, Dict (WellTyped x), VarAnn)
_ ::& HST xs
_), Natural
0) -> StackRef s -> Maybe (StackRef s)
forall a. a -> Maybe a
Just (PeanoNatural 'Z -> StackRef s
forall (st :: [T]) (idx :: Peano).
RequireLongerThan st idx =>
PeanoNatural idx -> StackRef st
T.StackRef PeanoNatural 'Z
forall (n :: Peano). (n ~ 'Z) => PeanoNatural n
Zero)
      (((Notes x, Dict (WellTyped x), VarAnn)
_ ::& 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 :: Peano).
RequireLongerThan st idx =>
PeanoNatural idx -> StackRef st
T.StackRef (PeanoNatural idx -> PeanoNatural ('S idx)
forall (n :: Peano) (m :: Peano).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural idx
ns)