-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

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

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

import Michelson.ErrorPos
import Michelson.TypeCheck.Error
import Michelson.TypeCheck.Helpers
import Michelson.TypeCheck.TypeCheck
import Michelson.TypeCheck.Types
import Michelson.Typed (Notes(..), converge, mkUType, notesT, withUType)
import qualified Michelson.Typed as T
import Michelson.Untyped
  (ExpandedOp, StackFn, TyVar(..), Type, Var, VarAnn, sfnInPattern, sfnOutPattern,
  sfnQuantifiedVars, varSet)
import qualified Michelson.Untyped as U
import Util.Peano (SingNat(SS, SZ))

type TypeCheckListHandler inp =
     [U.ExpandedOp]
  -> HST inp
  -> TypeCheck (SomeInstr inp)

typeCheckExt
  :: forall s.
     (Typeable s)
  => TypeCheckListHandler s
  -> U.ExpandedExtInstr
  -> HST s
  -> TypeCheckInstr (SomeInstr s)
typeCheckExt :: TypeCheckListHandler s
-> ExpandedExtInstr -> HST s -> TypeCheckInstr (SomeInstr s)
typeCheckExt typeCheckListH :: TypeCheckListHandler s
typeCheckListH ext :: ExpandedExtInstr
ext hst :: HST s
hst = do
  InstrCallStack
instrPos <- ReaderT InstrCallStack TypeCheck InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
  case ExpandedExtInstr
ext of
    U.STACKTYPE s :: StackTypePattern
s -> HST s
-> Either ExtError (SomeInstr s) -> TypeCheckInstr (SomeInstr s)
forall (s :: [T]) a.
Typeable 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
$ SomeInstr s
nopSomeInstr 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]).
Typeable xs =>
BoundVars
-> StackTypePattern -> HST xs -> Either ExtError BoundVars
checkStackType BoundVars
noBoundVars StackTypePattern
s HST s
hst
    U.FN t :: Text
t sf :: StackFn
sf op :: [ExpandedOp]
op  -> TypeCheckListHandler s
-> Text
-> StackFn
-> [ExpandedOp]
-> HST s
-> TypeCheckInstr (SomeInstr s)
forall (inp :: [T]).
Typeable inp =>
TypeCheckListHandler inp
-> Text
-> StackFn
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstr (SomeInstr inp)
checkFn TypeCheckListHandler s
typeCheckListH Text
t StackFn
sf [ExpandedOp]
op HST s
hst
    U.UPRINT pc :: PrintComment
pc   -> 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
<&> \tpc :: 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{..} -> do
      PrintComment -> TypeCheckInstr (PrintComment s)
verifyPrint PrintComment
tassComment
      _ :/ si :: SomeInstrOut s
si <- ExceptT TCError (State TypeCheckEnv) (SomeInstr s)
-> TypeCheckInstr (SomeInstr s)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT TCError (State TypeCheckEnv) (SomeInstr s)
 -> TypeCheckInstr (SomeInstr s))
-> ExceptT TCError (State TypeCheckEnv) (SomeInstr s)
-> TypeCheckInstr (SomeInstr s)
forall a b. (a -> b) -> a -> b
$ TypeCheckListHandler s
typeCheckListH [ExpandedOp]
tassInstrs HST s
hst
      case SomeInstrOut s
si of
        AnyOutInstr _ -> 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]). Typeable ts => HST ts -> SomeHST
SomeHST HST s
hst) InstrCallStack
instrPos (ExtError -> TCError) -> ExtError -> TCError
forall a b. (a -> b) -> a -> b
$ Text -> ExtError
TestAssertError
                         "TEST_ASSERT has to return Bool, but it always fails"
        instr :: Instr s out
instr ::: ((((Notes x, Dict (WellTyped x), VarAnn)
_ :: (T.Notes b, Dict (T.WellTyped b), VarAnn)) ::& (HST xs
_ :: HST out1))) -> 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]). Typeable ts => HST ts -> SomeHST
SomeHST HST s
hst) InstrCallStack
instrPos (ExtError -> TCError) -> ExtError -> TCError
forall a b. (a -> b) -> a -> b
$
                           Text -> ExtError
TestAssertError "TEST_ASSERT has to return Bool, but returned something else") (Either TCTypeError (x :~: 'TBool)
 -> Either TCError (x :~: 'TBool))
-> Either TCTypeError (x :~: 'TBool)
-> Either TCError (x :~: 'TBool)
forall a b. (a -> b) -> a -> b
$
                      Each '[KnownT] '[x, 'TBool] => Either TCTypeError (x :~: 'TBool)
forall (a :: T) (b :: T).
Each '[KnownT] '[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 (out :: [T]) (inp :: [T]).
Typeable out =>
Text
-> PrintComment inp -> Instr inp ('TBool : out) -> TestAssert inp
T.TestAssert Text
tassName PrintComment s
tcom Instr s out
Instr s ('TBool : xs)
instr
        _ ->
          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]). Typeable ts => HST ts -> SomeHST
SomeHST HST s
hst) InstrCallStack
instrPos (ExtError -> TCError) -> ExtError -> TCError
forall a b. (a -> b) -> a -> b
$
            Text -> ExtError
TestAssertError "TEST_ASSERT has to return Bool, but the stack is empty"
    U.UCOMMENT t :: 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
      SomeInstr s -> TypeCheckInstr (SomeInstr s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeInstr s -> TypeCheckInstr (SomeInstr s))
-> SomeInstr s -> TypeCheckInstr (SomeInstr 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 pc :: [Either Text StackRef]
pc) = do
      let checkStRef :: Either Text StackRef
-> ReaderT InstrCallStack TypeCheck (Either Text (StackRef s))
checkStRef (Left txt :: 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 i :: 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, Typeable 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 ext' :: 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]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST s
hst
    nopSomeInstr :: SomeInstr s
nopSomeInstr = HST s
hst HST s -> SomeInstrOut s -> SomeInstr s
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ Instr s s
forall (s :: [T]). Instr s s
T.Nop Instr s s -> HST s -> SomeInstrOut s
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST s
hst

liftExtError :: Typeable s => HST s -> Either ExtError a -> TypeCheckInstr a
liftExtError :: HST s -> Either ExtError a -> TypeCheckInstr a
liftExtError hst :: HST s
hst ei :: 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]). Typeable 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 t :: Text
t sf :: StackFn
sf = case StackFn -> Maybe (Set Var)
sfnQuantifiedVars StackFn
sf of
  Just qs :: 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
  _ -> Either ExtError ()
forall (f :: * -> *). Applicative f => f ()
pass

-- | Executes function body, pushing @ExtFrame@ onto the state and checks
-- the pattern in @FN@.
checkFn
  :: Typeable inp
  => TypeCheckListHandler inp
  -> Text
  -> StackFn
  -> [ExpandedOp]
  -> HST inp
  -> TypeCheckInstr (SomeInstr inp)
checkFn :: TypeCheckListHandler inp
-> Text
-> StackFn
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstr (SomeInstr inp)
checkFn typeCheckListH :: TypeCheckListHandler inp
typeCheckListH t :: Text
t sf :: StackFn
sf body :: [ExpandedOp]
body inp :: HST inp
inp = do
  BoundVars
vars <- HST inp -> ReaderT InstrCallStack TypeCheck BoundVars
checkStart HST inp
inp
  res :: SomeInstr inp
res@(_ :/ instr :: SomeInstrOut inp
instr) <- ExceptT TCError (State TypeCheckEnv) (SomeInstr inp)
-> TypeCheckInstr (SomeInstr inp)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT TCError (State TypeCheckEnv) (SomeInstr inp)
 -> TypeCheckInstr (SomeInstr inp))
-> ExceptT TCError (State TypeCheckEnv) (SomeInstr inp)
-> TypeCheckInstr (SomeInstr inp)
forall a b. (a -> b) -> a -> b
$ TypeCheckListHandler inp
typeCheckListH [ExpandedOp]
body HST inp
inp
  case SomeInstrOut inp
instr of
    _ ::: out :: HST out
out -> BoundVars -> HST out -> TypeCheckInstr ()
forall (out :: [T]).
Typeable out =>
BoundVars -> HST out -> TypeCheckInstr ()
checkEnd BoundVars
vars HST out
out
    AnyOutInstr _ -> TypeCheckInstr ()
forall (f :: * -> *). Applicative f => f ()
pass
  return SomeInstr inp
res
  where
    checkStart :: HST inp -> ReaderT InstrCallStack TypeCheck BoundVars
checkStart hst :: HST inp
hst = do
      HST inp -> Either ExtError () -> TypeCheckInstr ()
forall (s :: [T]) a.
Typeable 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
-> ReaderT InstrCallStack TypeCheck BoundVars
forall (s :: [T]) a.
Typeable s =>
HST s -> Either ExtError a -> TypeCheckInstr a
liftExtError HST inp
hst (Either ExtError BoundVars
 -> ReaderT InstrCallStack TypeCheck BoundVars)
-> Either ExtError BoundVars
-> ReaderT InstrCallStack TypeCheck BoundVars
forall a b. (a -> b) -> a -> b
$ BoundVars
-> StackTypePattern -> HST inp -> Either ExtError BoundVars
forall (xs :: [T]).
Typeable 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 :: Typeable out => BoundVars -> HST out -> TypeCheckInstr ()
    checkEnd :: BoundVars -> HST out -> TypeCheckInstr ()
checkEnd vars :: BoundVars
vars out :: HST out
out = HST out -> Either ExtError () -> TypeCheckInstr ()
forall (s :: [T]) a.
Typeable 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]).
Typeable xs =>
BoundVars
-> StackTypePattern -> HST xs -> Either ExtError BoundVars
checkStackType BoundVars
vars (StackFn -> StackTypePattern
sfnOutPattern StackFn
sf) HST out
out

-- | Check that a @StackTypePattern@ matches the type of the current stack
checkStackType
  :: Typeable xs
  => BoundVars
  -> U.StackTypePattern
  -> HST xs
  -> Either ExtError BoundVars
checkStackType :: BoundVars
-> StackTypePattern -> HST xs -> Either ExtError BoundVars
checkStackType (BoundVars vars :: Map Var Type
vars boundStkRest :: Maybe SomeHST
boundStkRest) s :: StackTypePattern
s hst :: HST xs
hst = Map Var Type
-> Int -> StackTypePattern -> HST xs -> Either ExtError BoundVars
forall (xs :: [T]).
Typeable xs =>
Map Var Type
-> Int -> StackTypePattern -> HST xs -> Either ExtError BoundVars
go Map Var Type
vars 0 StackTypePattern
s HST xs
hst
  where
    go :: Typeable xs => Map Var Type -> Int -> U.StackTypePattern -> HST xs
       -> Either ExtError BoundVars
    go :: Map Var Type
-> Int -> StackTypePattern -> HST xs -> Either ExtError BoundVars
go m :: Map Var Type
m _ U.StkRest sr :: HST xs
sr = case Maybe SomeHST
boundStkRest of
      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 Type -> Maybe SomeHST -> BoundVars
BoundVars Map Var Type
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]). Typeable ts => HST ts -> SomeHST
SomeHST HST xs
sr)
      Just si :: SomeHST
si@(SomeHST sr' :: 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]). Typeable 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 Type -> Maybe SomeHST -> BoundVars
BoundVars Map Var Type
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]).
(Typeable as, Typeable bs) =>
HST as -> HST bs -> Either TCTypeError (as :~: bs)
eqHST HST xs
sr HST ts
sr')
    go m :: Map Var Type
m _ U.StkEmpty 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 Type -> Maybe SomeHST -> BoundVars
BoundVars Map Var Type
m Maybe SomeHST
forall a. Maybe a
Nothing
    go _ _ U.StkEmpty _    = 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 _ _ _ 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 m :: Map Var Type
m n :: Int
n (U.StkCons tyVar :: TyVar
tyVar ts :: StackTypePattern
ts) ((Notes x
xann :: Notes xt, _, _) ::& xs :: HST xs
xs) =
      let
        handleType :: U.Type -> Either ExtError BoundVars
        handleType :: Type -> Either ExtError BoundVars
handleType t :: Type
t =
          Type
-> (forall (t :: T).
    KnownT t =>
    Notes t -> Either ExtError BoundVars)
-> Either ExtError BoundVars
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
withUType Type
t ((forall (t :: T).
  KnownT t =>
  Notes t -> Either ExtError BoundVars)
 -> Either ExtError BoundVars)
-> (forall (t :: T).
    KnownT 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
              (\_ -> StackTypePattern -> Int -> TCTypeError -> ExtError
TypeMismatch StackTypePattern
s Int
n (TCTypeError -> ExtError) -> TCTypeError -> ExtError
forall a b. (a -> b) -> a -> b
$ T -> T -> TCTypeError
TypeEqError (Notes x -> T
forall (t :: T). SingI t => Notes t -> T
notesT Notes x
xann) (Notes t -> T
forall (t :: T). SingI t => Notes t -> T
notesT Notes t
tann))
              (Each '[KnownT] '[x, t] => Either TCTypeError (x :~: t)
forall (a :: T) (b :: T).
Each '[KnownT] '[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 Type
-> Int -> StackTypePattern -> HST xs -> Either ExtError BoundVars
forall (xs :: [T]).
Typeable xs =>
Map Var Type
-> Int -> StackTypePattern -> HST xs -> Either ExtError BoundVars
go Map Var Type
m (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) StackTypePattern
ts HST xs
xs
      in case TyVar
tyVar of
        TyCon t :: Type
t -> Type -> Either ExtError BoundVars
handleType Type
t
        VarID v :: Var
v -> case Var -> Map Var Type -> Maybe Type
forall k a. Ord k => k -> Map k a -> Maybe a
lookup Var
v Map Var Type
m of
          Nothing -> let t :: Type
t = Notes x -> Type
forall (x :: T). SingI x => Notes x -> Type
mkUType Notes x
xann in Map Var Type
-> Int -> StackTypePattern -> HST xs -> Either ExtError BoundVars
forall (xs :: [T]).
Typeable xs =>
Map Var Type
-> Int -> StackTypePattern -> HST xs -> Either ExtError BoundVars
go (Var -> Type -> Map Var Type -> Map Var Type
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert Var
v Type
t Map Var Type
m) (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) StackTypePattern
ts HST xs
xs
          Just t :: Type
t -> Type -> Either ExtError BoundVars
handleType Type
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, Typeable s)
  => Natural -> HST s -> m (T.StackRef s)
createStackRef :: Natural -> HST s -> m (StackRef s)
createStackRef idx :: Natural
idx hst :: 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 sr :: StackRef s
sr -> StackRef s -> m (StackRef s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackRef s
sr
    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]). Typeable 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
      (SNil, _) -> Maybe (StackRef s)
forall a. Maybe a
Nothing
      ((_ ::& _), 0) -> StackRef s -> Maybe (StackRef s)
forall a. a -> Maybe a
Just (Sing 'Z -> StackRef s
forall (idx :: Peano) (st :: [T]).
(KnownPeano idx, SingI idx, RequireLongerThan st idx) =>
Sing idx -> StackRef st
T.StackRef Sing 'Z
SingNat 'Z
SZ)
      ((_ ::& st :: HST xs
st), i :: Natural
i) -> do
        T.StackRef ns :: Sing 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
- 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
$ Sing ('S idx) -> StackRef s
forall (idx :: Peano) (st :: [T]).
(KnownPeano idx, SingI idx, RequireLongerThan st idx) =>
Sing idx -> StackRef st
T.StackRef (SingNat idx -> SingNat ('S idx)
forall (n :: Peano).
(SingI n, KnownPeano n) =>
SingNat n -> SingNat ('S n)
SS Sing idx
SingNat idx
ns)