morley-1.4.0: src/Michelson/TypeCheck/Instr.hs
-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ
-- | Module, providing functions for conversion from
-- instruction and value representation from @Michelson.Type@ module
-- to strictly-typed GADT-based representation from @Michelson.Value@ module.
--
-- This conversion is labeled as type check because that's what we are obliged
-- to do on our way.
--
-- Type check algorithm relies on the property of Michelson language that each
-- instruction on a given input stack type produces a definite output stack
-- type.
-- Michelson contract defines concrete types for storage and parameter, from
-- which input stack type is deduced. Then this type is being combined with
-- each subsequent instruction, producing next stack type after each
-- application.
--
-- Function @typeCheck@ takes list of instructions and returns value of type
-- @Instr inp out@ along with @HST inp@ and @HST out@ all wrapped into
-- @SomeInstr@ data type. This wrapping is done to satsify Haskell type
-- system (which has no support for dependent types).
-- Functions @typeCheckInstr@, @typeCheckValue@ behave similarly.
--
-- When a recursive call is made within @typeCheck@, @typeCheckInstr@ or
-- @typeCheckValue@, result of a call is unwrapped from @SomeInstr@ and type
-- information from @HST inp@ and @HST out@ is being used to assert that
-- recursive call returned instruction of expected type
-- (error is thrown otherwise).
module Michelson.TypeCheck.Instr
( typeCheckContract
, typeCheckValue
, typeCheckList
, typeVerifyTopLevelType
, typeCheckTopLevelType
) where
import Prelude hiding (EQ, GT, LT)
import Control.Monad.Except (MonadError, liftEither, throwError)
import Data.Default (def)
import Data.Generics (everything, mkQ)
import Data.Singletons (Sing, demote)
import Data.Typeable ((:~:)(..))
import Michelson.ErrorPos
import Michelson.TypeCheck.Error
import Michelson.TypeCheck.Ext
import Michelson.TypeCheck.Helpers
import Michelson.TypeCheck.TypeCheck
import Michelson.TypeCheck.Types
import Michelson.TypeCheck.Value
import Michelson.Typed.Value
import Michelson.Typed
import Util.Peano
import qualified Michelson.Untyped as U
import Michelson.Untyped.Annotation (VarAnn)
typeCheckContract
:: TcOriginatedContracts
-> U.Contract
-> Either TCError SomeContract
typeCheckContract cs c =
runTypeCheck (U.contractParameter c) cs $ typeCheckContractImpl c
withWTP :: forall t a. SingI t => (WellTyped t => TypeCheck a) -> TypeCheck a
withWTP fn = case getWTP @t of
Just Dict -> fn
Nothing -> throwError $ TCContractError "Not a well typed value" Nothing
withWTPInstr_ :: forall t a. SingI t => U.ExpandedInstr -> SomeHST -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
withWTPInstr_ v t fn = case getWTP @t of
Just Dict -> fn
Nothing -> do
loc <- ask
throwError $ TCFailedOnInstr v t loc Nothing (Just $ UnsupportedTypeForScope (demote @t) BtNotComparable)
typeCheckContractImpl
:: U.Contract
-> TypeCheck SomeContract
typeCheckContractImpl (U.Contract (U.ParameterType mParam rootAnn) mStorage pCode) = do
_ <- maybe (throwError $ TCContractError "no instructions in contract code" $ Just EmptyCode)
pure (nonEmpty pCode)
withUType mParam $ \(paramNote :: Notes param) ->
withUType mStorage $ \(storageNote :: Notes st) -> do
withWTP @st $ do
withWTP @param $ do
Dict <- either (hasTypeError @param "parameter") pure
$ checkScope @(ParameterScope param)
Dict <- either (hasTypeError @st "storage") pure
$ checkScope @(StorageScope st)
let inpNote = NTPair def def def paramNote storageNote
let inp = (inpNote, Dict, def) ::& SNil
inp' :/ instrOut <- usingReaderT def $ typeCheckImpl typeCheckInstr pCode inp
let (paramNotesRaw, cStoreNotes) = case inp' of
(NTPair _ _ _ cpNotes stNotes, _, _) ::& SNil -> (cpNotes, stNotes)
cParamNotes <-
liftEither $
mkParamNotes paramNotesRaw rootAnn `onLeft`
(TCContractError "invalid parameter declaration: " . Just . IllegalParamDecl)
case instrOut of
instr ::: out -> liftEither $ do
case eqHST1 @(ContractOut1 st) out of
Right Refl -> do
let (outN, _, _) ::& SNil = out
_ <- converge outN (NTPair def def def starNotes storageNote)
`onLeft`
((TCContractError "contract output type violates convention:") . Just . AnnError)
pure $ SomeContract Contract
{ cCode = instr
, cParamNotes
, cStoreNotes
}
Left err -> Left $ TCContractError "contract output type violates convention:" $ Just err
AnyOutInstr instr ->
pure $ SomeContract Contract
{ cCode = instr
, cParamNotes
, cStoreNotes
}
where
hasTypeError :: forall (t :: T) a. SingI t => Text -> BadTypeForScope -> TypeCheck a
hasTypeError name reason = throwError $
TCContractError ("contract " <> name <> " type error") $
Just $ UnsupportedTypeForScope (demote @t) reason
-- | Function @typeCheckList@ converts list of Michelson instructions
-- given in representation from @Michelson.Type@ module to representation
-- in strictly typed GADT.
--
-- Types are checked along the way which is neccessary to construct a
-- strictly typed value.
--
-- As a second argument, @typeCheckList@ accepts input stack type representation.
typeCheckList
:: (Typeable inp)
=> [U.ExpandedOp]
-> HST inp
-> TypeCheck (SomeInstr inp)
typeCheckList = usingReaderT def ... typeCheckImpl typeCheckInstr
-- | Function @typeCheckValue@ converts a single Michelson value
-- given in representation from @Michelson.Untyped@ module hierarchy to
-- representation in strictly typed GADT.
--
-- @typeCheckValue@ is polymorphic in the expected type of value.
--
-- Type checking algorithm pattern-matches on parse value representation,
-- expected type @t@ and constructs @Val t@ value.
--
-- If there was no match on a given pair of value and expected type,
-- that is interpreted as input of wrong type and type check finishes with
-- error.
typeCheckValue
:: forall t.
(SingI t)
=> U.Value
-> TypeCheckInstr (Value t)
typeCheckValue = typeCheckValImpl @t typeCheckInstr
typeVerifyTopLevelType
:: (SingI t, HasCallStack)
=> TcOriginatedContracts -> U.Value -> Either TCError (Value t)
typeVerifyTopLevelType originatedContracts valueU =
runTypeCheck param originatedContracts $ usingReaderT (def :: InstrCallStack) $
typeCheckValue valueU
where
param = error "parameter type touched during top-level type typecheck"
typeCheckTopLevelType
:: HasCallStack
=> TcOriginatedContracts -> U.Type -> U.Value -> Either TCError SomeValue
typeCheckTopLevelType originatedContracts typeU valueU =
withSomeSingT (fromUType typeU) $ \(_ :: Sing t) ->
SomeValue <$> typeVerifyTopLevelType @t originatedContracts valueU
-- Helper data type we use to typecheck DROPN.
data TCDropHelper inp where
TCDropHelper ::
forall (n :: Peano) inp out.
(Typeable out, SingI n, KnownPeano n, LongerOrSameLength inp n, Drop n inp ~ out) =>
Sing n -> HST out -> TCDropHelper inp
-- Helper data type we use to typecheck DIG.
data TCDigHelper inp where
TCDigHelper ::
forall (n :: Peano) inp out a.
(Typeable out, ConstraintDIG n inp out a) =>
Sing n -> HST out -> TCDigHelper inp
-- Helper data type we use to typecheck DUG.
data TCDugHelper inp where
TCDugHelper ::
forall (n :: Peano) inp out a.
(Typeable out, ConstraintDUG n inp out a) =>
Sing n -> HST out -> TCDugHelper inp
-- | Function @typeCheckInstr@ converts a single Michelson instruction
-- given in representation from @Michelson.Type@ module to representation
-- in strictly typed GADT.
--
-- As a second argument, @typeCheckInstr@ accepts input stack type representation.
--
-- Type checking algorithm pattern-matches on given instruction, input stack
-- type and constructs strictly typed GADT value, checking necessary type
-- equalities when neccessary.
--
-- If there was no match on a given pair of instruction and input stack,
-- that is interpreted as input of wrong type and type check finishes with
-- error.
typeCheckInstr :: TcInstrHandler
typeCheckInstr uInstr inp = case (uInstr, inp) of
(U.EXT ext, si) ->
typeCheckExt typeCheckList ext si
(U.DROP, _ ::& rs) -> pure (inp :/ DROP ::: rs)
(U.DROP, SNil) -> notEnoughItemsOnStack
(U.DROPN nTotal, inputHST) ->
go nTotal inputHST <&> \case
TCDropHelper s out -> inputHST :/ DROPN s ::: out
where
go :: forall inp. Typeable inp
=> Word
-> HST inp
-> TypeCheckInstr (TCDropHelper inp)
go n i = case (n, i) of
(0, _) -> pure (TCDropHelper SZ i)
(_, SNil) -> notEnoughItemsOnStack
(_, (_ ::& iTail)) -> do
go (n - 1) iTail <&> \case TCDropHelper s out -> TCDropHelper (SS s) out
(U.DUP _vn, a ::& rs) ->
pure (inp :/ DUP ::: (a ::& a::& rs))
(U.DUP _vn, SNil) -> notEnoughItemsOnStack
(U.SWAP, a ::& b ::& rs) ->
pure (inp :/ SWAP ::: (b ::& a ::& rs))
(U.SWAP, _) -> notEnoughItemsOnStack
(U.DIG nTotal, inputHST) ->
go nTotal inputHST <&> \case
TCDigHelper s out -> inputHST :/ DIG s ::: out
where
go :: forall inp. Typeable inp
=> Word
-> HST inp
-> TypeCheckInstr (TCDigHelper inp)
go n i = case (n, i) of
-- Even 'DIG 0' is invalid on empty stack (so it is not strictly `Nop`).
(_, SNil) -> notEnoughItemsOnStack
(0, (_ ::& _)) -> pure (TCDigHelper SZ i)
(_, (b ::& iTail)) ->
go (n - 1) iTail <&> \case
TCDigHelper s (a ::& resTail) -> TCDigHelper (SS s) (a ::& b ::& resTail)
(U.DUG nTotal, inputHST) ->
go nTotal inputHST <&> \case
TCDugHelper s out -> inputHST :/ DUG s ::: out
where
go :: forall inp. Typeable inp
=> Word
-> HST inp
-> TypeCheckInstr (TCDugHelper inp)
go n i = case (n, i) of
(0, (_ ::& _)) -> pure (TCDugHelper SZ i)
(_, (a ::& b ::& iTail)) ->
go (n - 1) (a ::& iTail) <&> \case
TCDugHelper s resTail -> TCDugHelper (SS s) (b ::& resTail)
-- Two cases:
-- 1. Input stack is empty.
-- 2. n > 0 and input stack has exactly 1 item.
_ -> notEnoughItemsOnStack
(U.PUSH vn mt mval, i) ->
withUType mt $ \(nt :: Notes t) -> do
val <- typeCheckValue @t mval
proofScope <- onScopeCheckInstrErr @t uInstr (SomeHST i) Nothing
$ checkScope @(ConstantScope t)
case proofScope of
Dict -> withWTPInstr @t $ pure $ i :/ PUSH val ::: ((nt, Dict, vn) ::& i)
(U.SOME tn vn, (an, Dict, _) ::& rs) -> do
pure (inp :/ SOME ::: ((NTOption tn an, Dict, vn) ::& rs))
(U.SOME _ _, SNil) -> notEnoughItemsOnStack
(U.NONE tn vn elMt, _) ->
withUType elMt $ \(elNotes :: Notes t) ->
withWTPInstr @t $
pure $ inp :/ NONE ::: ((NTOption tn elNotes, Dict, vn) ::& inp)
(U.UNIT tn vn, _) ->
pure $ inp :/ UNIT ::: ((NTUnit tn, Dict, vn) ::& inp)
(U.IF_NONE mp mq, (STOption{}, (ons :: Notes ('TOption a)), Dict, ovn) ::&+ rs) -> do
let (an, avn) = deriveNsOption ons ovn
withWTPInstr @a $
genericIf IF_NONE U.IF_NONE mp mq rs ((an, Dict, avn) ::& rs) inp
(U.IF_NONE _ _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectOption Nothing :| []) :| []
(U.IF_NONE _ _, SNil) -> notEnoughItemsOnStack
(U.PAIR tn vn pfn qfn, (an, _, avn) ::& (bn, _, bvn) ::& rs) -> do
let (vn', pfn', qfn') = deriveSpecialFNs pfn qfn avn bvn
case NTPair tn pfn' qfn' an bn of
(ns :: Notes ('TPair a b)) -> withWTPInstr @('TPair a b) $ pure (inp :/ PAIR ::: ((ns, Dict, vn `orAnn` vn') ::& rs))
(U.PAIR {}, _) -> notEnoughItemsOnStack
(U.CAR vn fn, (STPair{}, NTPair pairTN pfn qfn (pns :: Notes p) (qns :: Notes q), _, pairVN) ::&+ rs) -> do
pfn' <- onTypeCheckInstrAnnErr uInstr inp (Just CarArgument) (convergeAnns fn pfn)
withWTPInstr @p $
withWTPInstr @('TPair p q) $ do
let vn' = deriveSpecialVN vn pfn' pairVN
i' = (NTPair pairTN pfn' qfn pns qns, Dict, pairVN) ::& rs
pure $ i' :/ AnnCAR fn ::: ((pns, Dict, vn') ::& rs)
(U.CAR _ _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectPair Nothing Nothing :| []) :| []
(U.CAR _ _, SNil) -> notEnoughItemsOnStack
(U.CDR vn fn, (STPair{}, NTPair pairTN pfn qfn (pns :: Notes p) (qns :: Notes q), _, pairVN) ::&+ rs) -> do
qfn' <- onTypeCheckInstrAnnErr uInstr inp (Just CdrArgument) (convergeAnns fn qfn)
withWTPInstr @q $
withWTPInstr @('TPair p q) $ do
let vn' = deriveSpecialVN vn qfn' pairVN
i' = (NTPair pairTN pfn qfn' pns qns, Dict, pairVN) ::& rs
pure $ i' :/ AnnCDR fn ::: ((qns, Dict, vn') ::& rs)
(U.CDR _ _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectPair Nothing Nothing :| []) :| []
(U.CDR _ _, SNil) -> notEnoughItemsOnStack
(U.LEFT tn vn pfn qfn bMt, (an :: Notes l, Dict, _) ::& rs) ->
withUType bMt $ \(bn :: Notes r) -> do
withWTPInstr @r $ do
let ns = NTOr tn pfn qfn an bn
pure (inp :/ LEFT ::: ((ns, Dict, vn) ::& rs))
(U.LEFT {}, SNil) -> notEnoughItemsOnStack
(U.RIGHT tn vn pfn qfn aMt, (bn :: Notes r, Dict, _) ::& rs) ->
withUType aMt $ \(an :: Notes l) -> do
withWTPInstr @l $ do
let ns = NTOr tn pfn qfn an bn
pure (inp :/ RIGHT ::: ((ns, Dict, vn) ::& rs))
( U.RIGHT {}, SNil) -> notEnoughItemsOnStack
(U.IF_LEFT mp mq, (STOr{}, ons, _, ovn) ::&+ rs) -> do
case deriveNsOr ons ovn of
(an :: Notes a, bn :: Notes b, avn, bvn) ->
withWTPInstr @a $
withWTPInstr @b $ do
let
ait = (an, Dict, avn) ::& rs
bit = (bn, Dict, bvn) ::& rs
genericIf IF_LEFT U.IF_LEFT mp mq ait bit inp
(U.IF_LEFT _ _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectOr Nothing Nothing :| []) :| []
(U.IF_LEFT _ _, SNil) -> notEnoughItemsOnStack
(U.NIL tn vn elMt, i) ->
withUType elMt $ \(elNotes :: Notes t) ->
withWTPInstr @('TList t) $
pure $ i :/ NIL ::: ((NTList tn elNotes, Dict, vn) ::& i)
(U.CONS vn, ((an :: Notes a), _, _)
::& ((ln :: Notes l), _, _) ::& rs) ->
case eqType @('TList a) @l of
Right Refl -> do
(n :: Notes t) <- onTypeCheckInstrAnnErr uInstr inp (Just ConsArgument) (converge ln (NTList def an))
withWTPInstr @t $
pure $ inp :/ CONS ::: ((n, Dict, vn) ::& rs)
Left m -> typeCheckInstrErr' uInstr (SomeHST inp) (Just ConsArgument) m
(U.CONS _, _) -> notEnoughItemsOnStack
(U.IF_CONS mp mq, (STList{}, ns, Dict, vn) ::&+ rs) -> do
case ns of
NTList _ (an :: Notes t1) -> do
ait <- withWTPInstr @t1 $ pure $ (an, Dict, vn <> "hd") ::& (ns, Dict, vn <> "tl") ::& rs
genericIf IF_CONS U.IF_CONS mp mq ait rs inp
(U.IF_CONS _ _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectList Nothing :| []) :| []
(U.IF_CONS _ _, SNil)-> notEnoughItemsOnStack
(U.SIZE vn, (NTList{}, _, _) ::& _) -> sizeImpl inp vn
(U.SIZE vn, (NTSet{}, _, _) ::& _) -> sizeImpl inp vn
(U.SIZE vn, (NTMap{}, _, _) ::& _) -> sizeImpl inp vn
(U.SIZE vn, (NTString{}, _, _) ::& _) -> sizeImpl inp vn
(U.SIZE vn, (NTBytes{}, _, _) ::& _) -> sizeImpl inp vn
(U.SIZE _, _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectList Nothing :| []) :|
[ (ExpectSet Nothing :| [])
, (ExpectMap :| [])
, (ExpectString :| [])
, (ExpectByte :| [])
]
(U.SIZE _, SNil) -> notEnoughItemsOnStack
(U.EMPTY_SET tn vn mv, i) ->
withUType mv $ \(vns :: Notes v) ->
withWTPInstr @('TSet v) $
withCompareableCheck (notesSing vns) uInstr inp $ i :/ EMPTY_SET ::: ((STSet sing, NTSet tn vns, Dict, vn) ::&+ i)
(U.EMPTY_MAP tn vn mk mv, i) -> do
withUType mv $ \(vns :: Notes v) ->
withUType mk $ \(ktn :: Notes k) ->
withWTPInstr @('TMap k v) $
withCompareableCheck (notesSing ktn) uInstr inp $ i :/ EMPTY_MAP ::: ((STMap sing sing, NTMap tn ktn vns, Dict, vn) ::&+ i)
(U.EMPTY_BIG_MAP tn vn mk mv, i) ->
withUType mv $ \(vns :: Notes v) ->
withUType mk $ \(ktn :: Notes k) ->
withWTPInstr @('TBigMap k v) $
withCompareableCheck (notesSing ktn) uInstr inp $ i :/ EMPTY_BIG_MAP ::: ((STBigMap sing sing, NTBigMap tn ktn vns, Dict, vn) ::&+ i)
(U.MAP vn mp, (STList _, NTList _ (vns :: Notes t1), Dict, _vn) ::&+ _) -> do
withWTPInstr @t1 $
mapImpl vns uInstr mp inp
(\(rn :: Notes t) hst -> withWTPInstr @t $ pure $ (NTList def rn, Dict, vn) ::& hst)
(U.MAP vn mp, (STMap{}, NTMap _ kns vns, Dict, _vn) ::&+ _) -> do
case NTPair def def def kns vns of
(pns :: Notes ('TPair k v1)) ->
withWTPInstr @('TPair k v1) $
mapImpl pns uInstr mp inp
(\(rn :: Notes v) hst -> withWTPInstr @('TMap k v) $ pure $ (NTMap def kns rn, Dict, vn) ::& hst)
(U.MAP _ _, _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectList Nothing :| []) :|
[ (ExpectMap :| [])
]
(U.MAP _ _, SNil) -> notEnoughItemsOnStack
(U.ITER is, (STSet (_ :: Sing t1), NTSet _ en, _, _) ::&+ _) -> do
withWTPInstr @t1 $
iterImpl en uInstr is inp
(U.ITER is, (STList (_ :: Sing t1), NTList _ en, _, _) ::&+ _) -> do
withWTPInstr @t1 $
iterImpl en uInstr is inp
(U.ITER is, (STMap _ _, NTMap _ kns vns, _, _) ::&+ _) -> do
case NTPair def def def kns vns of
(en :: Notes ('TPair a b)) ->
withWTPInstr @('TPair a b) $ iterImpl en uInstr is inp
(U.ITER _, _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectSet Nothing :| []) :|
[ (ExpectList Nothing :| [])
, (ExpectMap :| [])
]
(U.ITER _, SNil) -> notEnoughItemsOnStack
(U.MEM varNotes,
_ ::& (STSet{}, NTSet _ notesK, _, _) ::&+ _) ->
memImpl notesK inp varNotes
(U.MEM varNotes,
_ ::& (STMap{}, NTMap _ notesK _, _, _) ::&+ _) ->
memImpl notesK inp varNotes
(U.MEM varNotes,
_ ::& (STBigMap{}, NTBigMap _ notesK _, _, _) ::&+ _) ->
memImpl notesK inp varNotes
(U.MEM _, _ ::& _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectTypeVar :| [ExpectSet Nothing]) :|
[ (ExpectTypeVar :| [ExpectMap])
, (ExpectTypeVar :| [ExpectBigMap])
]
(U.MEM _, _) -> notEnoughItemsOnStack
(U.GET varNotes,
_ ::& (STMap{}, NTMap _ notesK (notesV :: Notes v), _, _) ::&+ _) ->
withWTPInstr @v $ getImpl notesK inp notesV varNotes
(U.GET varNotes,
_ ::& (STBigMap{}, NTBigMap _ notesK (notesV :: Notes v), _, _) ::&+ _) ->
withWTPInstr @v $ getImpl notesK inp notesV varNotes
(U.GET _, _ ::& _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectTypeVar :| [ExpectMap]) :|
[ (ExpectTypeVar :| [ExpectBigMap])
]
(U.GET _, _) -> notEnoughItemsOnStack
(U.UPDATE varNotes,
_ ::& _ ::& (STMap{}, (NTMap _ notesK (notesV :: Notes v)), _, _) ::&+ _) ->
updImpl notesK inp (NTOption U.noAnn notesV) varNotes
(U.UPDATE varNotes,
_ ::& _ ::& (STBigMap{}, NTBigMap _ notesK (notesV :: Notes v), _, _) ::&+ _) ->
updImpl notesK inp (NTOption U.noAnn notesV) varNotes
(U.UPDATE varNotes,
_ ::& _ ::& (STSet{}, NTSet _ (notesK :: Notes k), _, _) ::&+ _) ->
updImpl notesK inp (NTBool U.noAnn) varNotes
(U.UPDATE _, _ ::& _ ::& _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectTypeVar :| [ExpectTypeVar, ExpectMap]) :|
[ (ExpectTypeVar :| [ExpectTypeVar, ExpectBigMap])
, (ExpectTypeVar :| [ExpectTypeVar, ExpectSet Nothing])
]
(U.UPDATE _, _) -> notEnoughItemsOnStack
(U.IF mp mq, (NTBool{}, _, _) ::& rs) ->
genericIf IF U.IF mp mq rs rs inp
(U.IF _ _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectBool :| []) :| []
(U.IF _ _, SNil) -> notEnoughItemsOnStack
(U.LOOP is, (NTBool{}, _, _) ::& (rs :: HST rs)) -> do
_ :/ tp <- lift $ typeCheckList is rs
case tp of
subI ::: (o :: HST o) -> do
case eqHST o (sing @('TBool) -:& rs) of
Right Refl -> do
let _ ::& rs' = o
pure $ inp :/ LOOP subI ::: rs'
Left m -> typeCheckInstrErr' uInstr (SomeHST inp) (Just Iteration) m
AnyOutInstr subI ->
pure $ inp :/ LOOP subI ::: rs
(U.LOOP _, _ ::& _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectBool :| [ExpectStackVar]) :| []
(U.LOOP _, _) -> notEnoughItemsOnStack
(U.LOOP_LEFT is, (os@STOr{}, ons, Dict, ovn) ::&+ rs) -> do
case deriveNsOr ons ovn of
(an :: Notes t, bn :: Notes b, avn, bvn) -> do
withWTPInstr @t $ withWTPInstr @b $ do
let ait = (an, Dict, avn) ::& rs
_ :/ tp <- lift $ typeCheckList is ait
case tp of
subI ::: o -> do
case (eqHST o (os -:& rs), o) of
(Right Refl, ((ons', Dict, ovn') ::& rs')) -> do
let (_, bn', _, bvn') = deriveNsOr ons' ovn'
br <- onTypeCheckInstrAnnErr uInstr inp
(Just Iteration)
(convergeHSTEl (bn, Dict, bvn) (bn', Dict, bvn'))
pure $ inp :/ LOOP_LEFT subI ::: (br ::& rs')
(Left m, _) -> typeCheckInstrErr' uInstr (SomeHST inp) (Just Iteration) m
AnyOutInstr subI -> do
let br = (bn, Dict, bvn)
pure $ inp :/ LOOP_LEFT subI ::: (br ::& rs)
(U.LOOP_LEFT _, _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectOr Nothing Nothing :| [ExpectStackVar]) :| []
(U.LOOP_LEFT _, _) -> notEnoughItemsOnStack
(U.LAMBDA vn (AsUType (ins :: Notes t)) (AsUType (ons :: Notes u)) is, i) -> do
-- further processing is extracted into another function just not to
-- litter our main typechecking logic
withWTPInstr @t $
withWTPInstr @u $
lamImpl uInstr is vn ins ons i
(U.EXEC vn, ((_ :: Notes t1), _, _)
::& ( STLambda _ _
, NTLambda _ (_ :: Notes t1') (t2n :: Notes t2')
, _
, _
)
::&+ rs) -> do
Refl <- onTypeCheckInstrErr uInstr (SomeHST inp) (Just LambdaArgument)
(eqType @t1 @t1')
withWTPInstr @t2' $ pure $ inp :/ EXEC ::: ((t2n, Dict, vn) ::& rs)
(U.EXEC _, _ ::& _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectTypeVar :| [ExpectLambda Nothing Nothing]) :| []
(U.EXEC _, _) -> notEnoughItemsOnStack
(U.APPLY vn, ((_ :: Notes a'), _, _)
::& ( STLambda (STPair _ _) _
, NTLambda vann (NTPair _ _ _ (_ :: Notes a) (nb :: Notes b)) sc
, _
, _)
::&+ rs) -> do
case NTLambda vann nb sc of
(l2n :: Notes ('TLambda t1 t2)) -> withWTPInstr @('TLambda t1 t2) $ do
proofArgEq <- onTypeCheckInstrErr uInstr (SomeHST inp) (Just LambdaArgument)
(eqType @a' @a)
proofScope <- onScopeCheckInstrErr @a uInstr (SomeHST inp) (Just LambdaArgument)
$ checkScope @(ConstantScope a)
case (proofArgEq, proofScope) of
(Refl, Dict) ->
pure $ inp :/ (APPLY @a) ::: ((l2n, Dict, vn) ::& rs)
(U.APPLY _, _ ::& _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectTypeVar :| [ExpectLambda (Just $ ExpectPair Nothing Nothing) Nothing]) :| []
(U.APPLY _, _) -> notEnoughItemsOnStack
(U.DIP is, a ::& s) -> do
typeCheckDipBody uInstr is s $
\subI t -> pure $ inp :/ DIP subI ::: (a ::& t)
(U.DIP _is, SNil) -> notEnoughItemsOnStack
(U.DIPN nTotal instructions, inputHST) ->
go nTotal inputHST <&> \case
TCDipHelper s subI out -> inputHST :/ DIPN s subI ::: out
where
go :: forall inp. Typeable inp
=> Word
-> HST inp
-> TypeCheckInstr (TCDipHelper inp)
go n curHST = case (n, curHST) of
(0, _) -> typeCheckDipBody uInstr instructions curHST $ \subI t ->
pure (TCDipHelper SZ subI t)
(_, SNil) -> notEnoughItemsOnStack
(_, hstHead ::& hstTail) ->
go (n - 1) hstTail <&> \case
TCDipHelper s subI out -> TCDipHelper (SS s) subI (hstHead ::& out)
(u, v) -> case (u, v) of -- Workaround for not exceeding -fmax-pmcheck-iterations limit
(U.FAILWITH, (_ ::& _)) ->
pure $ inp :/ AnyOutInstr FAILWITH
(U.FAILWITH, _) -> notEnoughItemsOnStack
(U.CAST vn (AsUType (castToNotes :: Notes t)), (en, _, evn) ::& rs) -> do
(Refl, _) <- errM $ matchTypes en castToNotes
withWTPInstr @t $
pure $ inp :/ CAST ::: ((castToNotes, Dict, vn `orAnn` evn) ::& rs)
where
errM :: (MonadReader InstrCallStack m, MonadError TCError m) => Either TCTypeError a -> m a
errM = onTypeCheckInstrErr uInstr (SomeHST inp) (Just Cast)
(U.CAST _ _, _) -> notEnoughItemsOnStack
(U.RENAME vn, (an, Dict, _) ::& rs) ->
pure $ inp :/ RENAME ::: ((an, Dict, vn) ::& rs)
(U.RENAME _, SNil) -> notEnoughItemsOnStack
(U.UNPACK tn vn mt, (NTBytes{}, _, _) ::& rs) ->
withUType mt $ \(tns :: Notes tn) -> do
case NTOption tn tns of
(ns :: Notes ('TOption t1)) -> withWTPInstr @('TOption t1) $ do
Dict <- onScopeCheckInstrErr @tn uInstr (SomeHST inp) Nothing
$ checkScope @(UnpackedValScope tn)
pure $ inp :/ UNPACK ::: ((ns, Dict, vn) ::& rs)
(U.UNPACK {}, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectByte :| []) :| []
(U.UNPACK {}, SNil) -> notEnoughItemsOnStack
(U.PACK vn, (_ :: Notes a, _, _) ::& rs) -> do
Dict <- onScopeCheckInstrErr @a uInstr (SomeHST inp) Nothing
$ checkScope @(PackedValScope a)
pure $ inp :/ PACK ::: ((starNotes, Dict, vn) ::& rs)
(U.PACK _, SNil) -> notEnoughItemsOnStack
(U.CONCAT vn, (NTBytes{}, _, _) ::& (NTBytes{}, _, _) ::& _) ->
concatImpl inp vn
(U.CONCAT vn, (NTString{}, _, _) ::& (NTString{}, _, _) ::& _) ->
concatImpl inp vn
(U.CONCAT vn, (STList STBytes, _, _, _) ::&+ _) ->
concatImpl' inp vn
(U.CONCAT vn, (STList STString, _, _, _) ::&+ _) ->
concatImpl' inp vn
(U.CONCAT _, _ ::& _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectByte :| [ExpectByte]) :|
[ (ExpectString :| [ExpectString])
]
(U.CONCAT _, _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectList (Just ExpectByte) :| [ExpectList (Just ExpectByte)]) :|
[ (ExpectList (Just ExpectString) :| [ExpectList (Just ExpectString)])
]
(U.CONCAT _, SNil) -> notEnoughItemsOnStack
(U.SLICE vn, (NTNat{}, _, _) ::&
(NTNat{}, _, _) ::&
(NTString{}, _, _) ::& _) -> sliceImpl inp vn
(U.SLICE vn, (NTNat{}, _, _) ::&
(NTNat{}, _, _) ::&
(NTBytes{}, _, _) ::& _) -> sliceImpl inp vn
(U.SLICE _, _ ::& _ ::& _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectNat :| [ExpectNat, ExpectString]) :|
[ (ExpectNat :| [ExpectNat, ExpectByte])
]
(U.SLICE _, _) -> notEnoughItemsOnStack
(U.ISNAT vn', (NTInt{}, _, oldVn) ::& rs) -> do
let vn = vn' `orAnn` oldVn
pure $ inp :/ ISNAT ::: ((starNotes, Dict, vn) ::& rs)
(U.ISNAT _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []
(U.ISNAT _, SNil)-> notEnoughItemsOnStack
-- Type checking is already done inside `addImpl`.
(U.ADD vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> addImpl a b inp vn
(U.ADD _, _) -> notEnoughItemsOnStack
(U.SUB vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> subImpl a b inp vn
(U.SUB _, _) -> notEnoughItemsOnStack
(U.MUL vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> mulImpl a b inp vn
(U.MUL _, _) -> notEnoughItemsOnStack
(U.EDIV vn, (a, _, _, _) ::&+ (b, _, _, _) ::&+ _) -> edivImpl a b inp vn
(U.EDIV _, _) -> notEnoughItemsOnStack
(U.ABS vn, (STInt, _, _, _) ::&+ _) -> unaryArithImpl @Abs ABS inp vn
(U.ABS _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []
(U.ABS _, SNil) -> notEnoughItemsOnStack
(U.NEG vn, (STInt, _, _, _) ::&+ _) -> unaryArithImpl @Neg NEG inp vn
(U.NEG vn, (STNat, _, _, _) ::&+ _) -> unaryArithImpl @Neg NEG inp vn
(U.NEG _, _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectInt :| []) :|
[ (ExpectNat :| [])
]
(U.NEG _, SNil) -> notEnoughItemsOnStack
(U.LSL vn, (STNat, _, _, _) ::&+
(STNat, _, _, _) ::&+ _) -> arithImpl @Lsl LSL inp vn
(U.LSL _, _ ::& _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectNat :| [ExpectNat]) :| []
(U.LSL _, _) -> notEnoughItemsOnStack
(U.LSR vn, (STNat, _, _, _) ::&+
(STNat, _, _, _) ::&+ _) -> arithImpl @Lsr LSR inp vn
(U.LSR _, _ ::& _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectNat :| [ExpectNat]) :| []
(U.LSR _, _) -> notEnoughItemsOnStack
(U.OR vn, (STBool, _, _, _) ::&+
(STBool, _, _, _) ::&+ _) -> arithImpl @Or OR inp vn
(U.OR vn, (STNat, _, _, _) ::&+
(STNat, _, _, _) ::&+ _) -> arithImpl @Or OR inp vn
(U.OR _, _ ::& _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectBool :| [ExpectBool]) :|
[ (ExpectNat :| [ExpectNat])
]
(U.OR _, _) -> notEnoughItemsOnStack
(U.AND vn, (STInt, _, _, _) ::&+
(STNat, _, _, _) ::&+ _) -> arithImpl @And AND inp vn
(U.AND vn, (STNat, _, _, _) ::&+
(STNat, _, _, _) ::&+ _) -> arithImpl @And AND inp vn
(U.AND vn, (STBool, _, _, _) ::&+
(STBool, _, _, _) ::&+ _) -> arithImpl @And AND inp vn
(U.AND _, _ ::& _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectInt :| [ExpectNat]) :|
[ (ExpectNat :| [ExpectNat])
, (ExpectBool :| [ExpectBool])
]
(U.AND _, _) -> notEnoughItemsOnStack
(U.XOR vn, (STBool, _, _, _) ::&+
(STBool, _, _, _) ::&+ _) -> arithImpl @Xor XOR inp vn
(U.XOR vn, (STNat, _, _, _) ::&+
(STNat, _, _, _) ::&+ _) -> arithImpl @Xor XOR inp vn
(U.XOR _, _ ::& _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectBool :| [ExpectBool]) :|
[ (ExpectNat :| [ExpectNat])
]
(U.XOR _, _) -> notEnoughItemsOnStack
(U.NOT vn, (STNat, _, _, _) ::&+ _) -> unaryArithImpl @Not NOT inp vn
(U.NOT vn, (STBool, _, _, _) ::&+ _) -> unaryArithImpl @Not NOT inp vn
(U.NOT vn, (STInt, _, _, _) ::&+ _) -> unaryArithImpl @Not NOT inp vn
(U.NOT _, _ ::& _) ->
failWithErr $ UnexpectedType
$ (ExpectNat :| []) :|
[ (ExpectBool :| [])
, (ExpectInt :| [])
]
(U.NOT _, SNil) -> notEnoughItemsOnStack
(U.COMPARE vn,
(an :: Notes aT, _, _)
::& (bn :: Notes bT, _, _)
::& rs
)
-> do
case eqType @aT @bT of
Right Refl -> do
void . errConv $ converge an bn
proofScope <- onScopeCheckInstrErr @aT (U.COMPARE vn) (SomeHST inp) (Just ComparisonArguments)
$ checkScope @(ComparabilityScope aT)
case proofScope of
Dict ->
pure $ inp :/ COMPARE ::: ((starNotes, Dict, vn) ::& rs)
Left err -> do
typeCheckInstrErr' uInstr (SomeHST inp) (Just ComparisonArguments) err
where
errConv :: (MonadReader InstrCallStack m, MonadError TCError m) => Either AnnConvergeError a -> m a
errConv = onTypeCheckInstrAnnErr uInstr inp (Just ComparisonArguments)
(U.COMPARE _, _) -> notEnoughItemsOnStack
(U.EQ vn, (NTInt{}, _, _) ::& _) -> unaryArithImpl @Eq' EQ inp vn
(U.EQ _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []
(U.EQ _, SNil) -> notEnoughItemsOnStack
(U.NEQ vn, (NTInt{}, _, _) ::& _) -> unaryArithImpl @Neq NEQ inp vn
(U.NEQ _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []
(U.NEQ _, SNil) -> notEnoughItemsOnStack
(U.LT vn, (NTInt{}, _, _) ::& _) -> unaryArithImpl @Lt LT inp vn
(U.LT _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []
(U.LT _, SNil) -> notEnoughItemsOnStack
(U.GT vn, (NTInt{}, _, _) ::& _) -> unaryArithImpl @Gt GT inp vn
(U.GT _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []
(U.GT _, SNil) -> notEnoughItemsOnStack
(U.LE vn, (NTInt{}, _, _) ::& _) -> unaryArithImpl @Le LE inp vn
(U.LE _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []
(U.LE _, SNil) -> notEnoughItemsOnStack
(U.GE vn, (NTInt{}, _, _) ::& _) -> unaryArithImpl @Ge GE inp vn
(U.GE _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []
(U.GE _, SNil) -> notEnoughItemsOnStack
(U.INT vn, (NTNat{}, _, _) ::& rs) ->
pure $ inp :/ INT ::: ((starNotes, Dict, vn) ::& rs)
(U.INT _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectNat :| []) :| []
(U.INT _, SNil) -> notEnoughItemsOnStack
(U.SELF vn fn, _) -> do
(U.ParameterType cpType rootAnn) <- gets tcContractParam
-- Wrapping into 'ParamNotesUnsafe' is safe because originated contract has
-- valid parameter type
withUType cpType $ \((`ParamNotesUnsafe` rootAnn) -> notescp :: ParamNotes t) -> do
proofScope <- onScopeCheckInstrErr @t uInstr (SomeHST inp) (Just ContractParameter)
$ checkScope @(ParameterScope t)
case proofScope of
Dict -> do
epName <- onTypeCheckInstrErr uInstr (SomeHST inp) Nothing $
epNameFromRefAnn fn `onLeft` IllegalEntryPoint
MkEntryPointCallRes (argNotes :: Notes arg) epc <-
mkEntryPointCall epName notescp
& maybeToRight (EntryPointNotFound epName)
& onTypeCheckInstrErr uInstr (SomeHST inp) Nothing
case NTContract U.noAnn argNotes of
(ntRes :: Notes ('TContract t1)) ->
withWTPInstr @('TContract t1) $
pure $ inp :/ SELF @arg (SomeEpc epc) ::: ((ntRes, Dict, vn) ::& inp)
(U.CONTRACT vn fn mt, (NTAddress{}, _, _) ::& rs) ->
withUType mt $ \(tns :: Notes t) -> do
proofScope <- onScopeCheckInstrErr @t uInstr (SomeHST inp) (Just ContractParameter)
$ checkScope @(ParameterScope t)
let ns = NTOption def $ NTContract def tns
epName <- onTypeCheckInstrErr uInstr (SomeHST inp) Nothing
$ epNameFromRefAnn fn `onLeft` IllegalEntryPoint
case proofScope of
Dict ->
withWTPInstr @t $ pure $ inp :/ CONTRACT tns epName ::: ((ns, Dict, vn) ::& rs)
(U.CONTRACT {}, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectAddress :| []) :| []
(U.CONTRACT {}, SNil) -> notEnoughItemsOnStack
(U.TRANSFER_TOKENS vn, ((_ :: Notes p'), _, _)
::& (NTMutez{}, _, _)
::& (STContract (_ :: Sing p), _, _, _) ::&+ rs) -> do
proofScope <- onScopeCheckInstrErr @p uInstr (SomeHST inp) (Just ContractParameter)
$ checkScope @(ParameterScope p)
case (eqType @p @p', proofScope) of
(Right Refl, Dict) ->
pure $ inp :/ TRANSFER_TOKENS ::: ((starNotes, Dict, vn) ::& rs)
(Left m, _) ->
typeCheckInstrErr' uInstr (SomeHST inp) (Just ContractParameter) m
(U.TRANSFER_TOKENS _, _ ::& _ ::& _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectTypeVar :| [ExpectMutez, ExpectContract]) :| []
(U.TRANSFER_TOKENS _, _) -> notEnoughItemsOnStack
(U.SET_DELEGATE vn,
(STOption STKeyHash, NTOption _ NTKeyHash{}, _, _)
::&+ rs) -> do
pure $ inp :/ SET_DELEGATE ::: ((starNotes, Dict, vn) ::& rs)
(U.SET_DELEGATE _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectOption (Just ExpectKeyHash) :| []) :| []
(U.SET_DELEGATE _, _) -> notEnoughItemsOnStack
(U.CREATE_CONTRACT ovn avn contract,
(STOption STKeyHash, NTOption _ (_ :: Notes ('TKeyHash)), _, _)
::&+ (NTMutez{}, _, _)
::& (gn :: Notes g, Dict, _) ::& rs) -> do
(SomeContract
(Contract
(contr :: ContractCode p' g')
paramNotes
storeNotes))
<- lift $ typeCheckContractImpl contract
Refl <- onTypeCheckInstrErr uInstr (SomeHST inp) (Just ContractStorage)
$ eqType @g @g'
void $ onTypeCheckInstrAnnErr uInstr inp (Just ContractStorage) (converge gn storeNotes)
pure
$ inp :/ CREATE_CONTRACT (Contract contr paramNotes storeNotes)
::: ((starNotes, Dict, ovn) ::& (starNotes, Dict, avn) ::& rs)
(U.CREATE_CONTRACT {}, _ ::& _ ::& _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectOption Nothing :| [ExpectMutez, ExpectTypeVar]) :| []
(U.CREATE_CONTRACT {}, _) -> notEnoughItemsOnStack
(U.IMPLICIT_ACCOUNT vn, (NTKeyHash{}, _, _) ::& rs) ->
pure $ inp :/ IMPLICIT_ACCOUNT ::: ((starNotes, Dict, vn) ::& rs)
(U.IMPLICIT_ACCOUNT _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectKeyHash :| []) :| []
(U.IMPLICIT_ACCOUNT _, SNil) -> notEnoughItemsOnStack
(U.NOW vn, _) ->
pure $ inp :/ NOW ::: ((starNotes, Dict, vn) ::& inp)
(U.AMOUNT vn, _) ->
pure $ inp :/ AMOUNT ::: ((starNotes, Dict, vn) ::& inp)
(U.BALANCE vn, _) ->
pure $ inp :/ BALANCE ::: ((starNotes, Dict, vn) ::& inp)
(U.CHECK_SIGNATURE vn,
(NTKey _, _, _)
::& (NTSignature _, _, _) ::& (NTBytes{}, _, _) ::& rs) ->
pure $ inp :/ CHECK_SIGNATURE ::: ((starNotes, Dict, vn) ::& rs)
(U.CHECK_SIGNATURE _, _ ::& _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectKey :| [ExpectSignature]) :| []
(U.CHECK_SIGNATURE _, _) -> notEnoughItemsOnStack
(U.SHA256 vn, (NTBytes{}, _, _) ::& rs) ->
pure $ inp :/ SHA256 ::: ((starNotes, Dict, vn) ::& rs)
(U.SHA256 _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectByte :| []) :| []
(U.SHA256 _, SNil) -> notEnoughItemsOnStack
(U.SHA512 vn, (NTBytes{}, _, _) ::& rs) ->
pure $ inp :/ SHA512 ::: ((starNotes, Dict, vn) ::& rs)
(U.SHA512 _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectByte :| []) :| []
(U.SHA512 _, SNil) -> notEnoughItemsOnStack
(U.BLAKE2B vn, (NTBytes{}, _, _) ::& rs) ->
pure $ inp :/ BLAKE2B ::: ((starNotes, Dict, vn) ::& rs)
(U.BLAKE2B _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectByte :| []) :| []
(U.BLAKE2B _, SNil) -> notEnoughItemsOnStack
(U.HASH_KEY vn, (NTKey{}, _, _) ::& rs) ->
pure $ inp :/ HASH_KEY ::: ((starNotes, Dict, vn) ::& rs)
(U.HASH_KEY _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectKey :| []) :| []
(U.HASH_KEY _, SNil) -> notEnoughItemsOnStack
(U.SOURCE vn, _) ->
pure $ inp :/ SOURCE ::: ((starNotes, Dict, vn) ::& inp)
(U.SENDER vn, _) ->
pure $ inp :/ SENDER ::: ((starNotes, Dict, vn) ::& inp)
(U.ADDRESS vn, (NTContract{}, _, _) ::& rs) ->
pure $ inp :/ ADDRESS ::: ((starNotes, Dict, vn) ::& rs)
(U.ADDRESS _, _ ::& _) ->
failWithErr $ UnexpectedType $ (ExpectContract :| []) :| []
(U.ADDRESS _, SNil) -> notEnoughItemsOnStack
(U.CHAIN_ID vn, _) ->
pure $ inp :/ CHAIN_ID ::: ((starNotes, Dict, vn) ::& inp)
-- Could not get rid of the catch all clause due to this warning:
-- @
-- Pattern match checker exceeded (2000000) iterations in
-- a case alternative. (Use -fmax-pmcheck-iterations=n
-- to set the maximum number of iterations to n)
-- @
i ->
error $ "Pattern matches should be exhuastive, but instead got: " <> show i
where
withWTPInstr :: forall t a. SingI t => (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
withWTPInstr fn = withWTPInstr_ @t uInstr (SomeHST inp) fn
failWithErr :: (MonadReader InstrCallStack m, MonadError TCError m) => TCTypeError -> m a
failWithErr = typeCheckInstrErr' uInstr (SomeHST inp) Nothing
notEnoughItemsOnStack :: (MonadReader InstrCallStack m, MonadError TCError m) => m a
notEnoughItemsOnStack = failWithErr NotEnoughItemsOnStack
-- | Helper function for two-branch if where each branch is given a single
-- value.
genericIf
:: forall bti bfi cond rs .
(Typeable bti, Typeable bfi)
=> (forall s'.
Instr bti s' ->
Instr bfi s' ->
Instr (cond ': rs) s'
)
-> ([U.ExpandedOp] -> [U.ExpandedOp] -> U.ExpandedInstr)
-> [U.ExpandedOp]
-> [U.ExpandedOp]
-> HST bti
-> HST bfi
-> HST (cond ': rs)
-> TypeCheckInstr (SomeInstr (cond ': rs))
genericIf cons mCons mbt mbf bti bfi i@(_ ::& _) = do
_ :/ pinstr <- lift $ typeCheckList mbt bti
_ :/ qinstr <- lift $ typeCheckList mbf bfi
fmap (i :/) $ case (pinstr, qinstr) of
(p ::: po, q ::: qo) -> do
let instr = mCons mbt mbf
Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just If)
$ eqHST po qo
o <- onTypeCheckInstrAnnErr instr i (Just If) (convergeHST po qo)
pure $ cons p q ::: o
(AnyOutInstr p, q ::: qo) -> do
pure $ cons p q ::: qo
(p ::: po, AnyOutInstr q) -> do
pure $ cons p q ::: po
(AnyOutInstr p, AnyOutInstr q) ->
pure $ AnyOutInstr (cons p q)
mapImpl
:: forall c rs .
( MapOp c
, WellTyped (MapOpInp c)
, Typeable (MapOpRes c)
)
=> Notes (MapOpInp c)
-> U.ExpandedInstr
-> [U.ExpandedOp]
-> HST (c ': rs)
-> (forall v' . (KnownT v') =>
Notes v' -> HST rs -> TypeCheckInstr (HST (MapOpRes c v' ': rs)))
-> TypeCheckInstr (SomeInstr (c ': rs))
mapImpl vn instr mp i@(_ ::& rs) mkRes = do
_ :/ subp <- lift $ typeCheckList mp ((vn, Dict, def) ::& rs)
case subp of
sub ::: subo ->
case subo of
(bn, _, _bvn) ::& rs' -> do
Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just Iteration)
$ eqHST rs rs'
x <- mkRes bn rs'
pure $ i :/ MAP sub ::: x
_ -> typeCheckInstrErr instr (SomeHST i) (Just Iteration)
AnyOutInstr _ ->
typeCheckInstrErr' instr (SomeHST i) (Just Iteration) CodeAlwaysFails
iterImpl
:: forall c rs .
( IterOp c
, WellTyped (IterOpEl c)
)
=> Notes (IterOpEl c)
-> U.ExpandedInstr
-> [U.ExpandedOp]
-> HST (c ': rs)
-> TypeCheckInstr (SomeInstr (c ': rs))
iterImpl en instr mp i@((_, _, lvn) ::& rs) = do
let evn = deriveVN "elt" lvn
_ :/ subp <-
case mp of
[] -> typeCheckInstrErr' instr (SomeHST i) (Just Iteration) EmptyCode
_ -> typeCheckImpl typeCheckInstr mp ((en, Dict, evn) ::& rs)
case subp of
subI ::: o -> do
Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just Iteration)
$ eqHST o rs
pure $ i :/ ITER subI ::: o
AnyOutInstr _ ->
typeCheckInstrErr' instr (SomeHST i) (Just Iteration) CodeAlwaysFails
lamImpl
:: forall it ot ts .
( WellTyped it, WellTyped ot
, Typeable ts
)
=> U.ExpandedInstr
-> [U.ExpandedOp]
-> VarAnn
-> Notes it
-> Notes ot
-> HST ts
-> TypeCheckInstr (SomeInstr ts)
lamImpl instr is vn ins ons i = do
whenJust (getFirst $ foldMap hasSelf is) $ \selfInstr ->
typeCheckInstrErr' instr (SomeHST i) (Just LambdaCode) $ InvalidInstruction selfInstr
_ :/ lamI <- lift $ typeCheckList is ((ins, Dict, def) ::& SNil)
let lamNotes onsr = NTLambda def ins onsr
let lamSt onsr = (lamNotes onsr, Dict, vn) ::& i
fmap (i :/) $ case lamI of
lam ::: lo -> do
case eqHST1 @ot lo of
Right Refl -> do
let (ons', _, _) ::& SNil = lo
onsr <- onTypeCheckInstrAnnErr instr i (Just LambdaCode) (converge ons ons')
pure (LAMBDA (VLam $ RfNormal lam) ::: lamSt onsr)
Left m -> typeCheckInstrErr' instr (SomeHST i) (Just LambdaCode) m
AnyOutInstr lam ->
pure (LAMBDA (VLam $ RfAlwaysFails lam) ::: lamSt ons)
where
hasSelf :: U.ExpandedOp -> First U.ExpandedInstr
hasSelf = everything (<>)
(mkQ (First Nothing)
(\case
selfInstr@(U.SELF{} :: U.InstrAbstract U.ExpandedOp) -> First $ Just selfInstr
_ -> First Nothing
)
)
----------------------------------------------------------------------------
-- Helpers for DIP (n) typechecking
----------------------------------------------------------------------------
-- Helper data type we use to typecheck DIPN.
data TCDipHelper inp where
TCDipHelper ::
forall (n :: Peano) inp out s s'.
(Typeable out, ConstraintDIPN n inp out s s') =>
Sing n -> Instr s s' -> HST out -> TCDipHelper inp
typeCheckDipBody ::
forall inp r. Typeable inp
=> U.ExpandedInstr
-> [U.ExpandedOp]
-> HST inp
-> (forall out. Typeable out =>
Instr inp out -> HST out -> TypeCheckInstr r)
-> TypeCheckInstr r
typeCheckDipBody mainInstr instructions inputHST callback = do
_ :/ tp <- lift (typeCheckList instructions inputHST)
case tp of
AnyOutInstr _ ->
-- This may seem like we throw error because of despair, but in fact,
-- the reference implementation seems to behave exactly in this way -
-- if output stack of code block within @DIP@ occurs to be any, an
-- error "FAILWITH must be at tail position" is raised.
-- It is not allowed even in `DIP 0`.
typeCheckInstrErr' mainInstr (SomeHST inputHST) (Just DipCode) CodeAlwaysFails
subI ::: t -> callback subI t