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

module Morley.Michelson.TypeCheck.TypeCheck
  ( TcInstr
  , TcInstrBase
  , TcOriginatedContracts
  , TypeCheckEnv(..)
  , BigMapFinder
  , TypeCheckOptions(..)
  , TypeCheck
  , TypeCheckNoExcept
  , TypeCheckResult
  , runTypeCheck
  , TypeCheckInstr
  , TypeCheckInstrNoExcept
  , runTypeCheckIsolated
  , typeCheckingWith
  , liftNoExcept
  , throwingTcError
  , IsInstrOp (..)
  , preserving
  , preserving'
  , guarding
  , guarding_
  , tcEither
  , ask'
  , asks'
  , local'

  , tcModeL
  , TypeCheckMode(..)
  , SomeParamType(..)
  , mkSomeParamType
  , TypeCheckInstrEnv (..)
  , tcieErrorPos
  , tcieNotInView
  ) where

import Control.Lens (makeLenses)
import Control.Monad.Except (Except, MonadError, runExcept, throwError)
import Data.Constraint (Dict)
import Data.Data (Data)
import Data.Default (Default(..))
import Data.Singletons (demote)
import Fmt (Buildable, build)

import Morley.Michelson.ErrorPos (ErrorSrcPos)
import Morley.Michelson.TypeCheck.Error (TcError'(..), TcTypeError(..))
import Morley.Michelson.TypeCheck.TypeCheckedSeq
  (IllTypedInstr(..), TypeCheckedInstr, TypeCheckedOp(..), TypeCheckedSeq(..), someInstrToOp,
  tcsEither)
import Morley.Michelson.TypeCheck.Types
import Morley.Michelson.Typed qualified as T
import Morley.Michelson.Typed.Existential (SomeVBigMap)
import Morley.Michelson.Untyped qualified as U
import Morley.Tezos.Address (ContractHash)
import Morley.Util.Lens
import Morley.Util.MultiReader

-- | Environments avaliable during typecheck.
type TCEnvs op = '[TypeCheckEnv op, TypeCheckOptions]

-- | A full type-check monad carrying intermediary context (via 'TypeCheckEnv'),
-- general 'TypeCheckOptions' and throwing 'TcError\''.
type TypeCheck op = MultiReaderT (TCEnvs op) (Except (TcError' op))

-- | A non-throwing alternative for 'TypeCheck'. Mainly meant to be used for
-- construction of a partially typed tree (see 'TypeCheckedSeq').
type TypeCheckNoExcept op = MultiReaderT (TCEnvs op) Identity

-- | Monad for performing some typechecking operations with the same options.
--
-- Unlike 'TypeCheck' monad, this does not carry the context of intra-contract
-- or intra-value typechecking.
type TypeCheckResult op = ReaderT TypeCheckOptions (Except (TcError' op))

-- | Environments available during instr typecheck
type TCInstrEnvs op = TypeCheckInstrEnv ': TCEnvs op

-- | Version of 'TypeCheck' additionally carrying instruction-specific
-- 'TypeCheckInstrEnv'
type TypeCheckInstr op = MultiReaderT (TCInstrEnvs op) (Except (TcError' op))

-- | Version of 'TypeCheckNoExcept' additionally carrying instruction-specific
-- 'TypeCheckInstrEnv'
type TypeCheckInstrNoExcept op = MultiReaderT (TCInstrEnvs op) Identity

data SomeParamType = forall t. (T.ParameterScope t) =>
  SomeParamType (T.ParamNotes t)

-- | @Show@ instance of @SomeParamType@, mainly used in test.
deriving stock instance Show SomeParamType

-- | @Eq@ instance of @SomeParamType@, mainly used in test.
instance Eq SomeParamType where
  SomeParamType
s1 == :: SomeParamType -> SomeParamType -> Bool
== SomeParamType
s2 = SomeParamType -> ParameterType
someParamToParameterType SomeParamType
s1 ParameterType -> ParameterType -> Bool
forall a. Eq a => a -> a -> Bool
== SomeParamType -> ParameterType
someParamToParameterType SomeParamType
s2

-- | @Buildable@ instance of @SomeParamType@, mainly used in test.
instance Buildable SomeParamType where
  build :: SomeParamType -> Doc
build = ParameterType -> Doc
forall a. Buildable a => a -> Doc
build (ParameterType -> Doc)
-> (SomeParamType -> ParameterType) -> SomeParamType -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeParamType -> ParameterType
someParamToParameterType

-- | Helper function means to provide a quick way for creating instance
-- of @SomeParamType@ needed in test.
someParamToParameterType :: SomeParamType -> U.ParameterType
someParamToParameterType :: SomeParamType -> ParameterType
someParamToParameterType (SomeParamType T.UnsafeParamNotes{RootAnn
Notes t
pnNotes :: Notes t
pnRootAnn :: RootAnn
pnNotes :: forall (t :: T). ParamNotes t -> Notes t
pnRootAnn :: forall (t :: T). ParamNotes t -> RootAnn
..}) =
  Ty -> RootAnn -> ParameterType
U.ParameterType (Notes t -> Ty
forall (t :: T). SingI t => Notes t -> Ty
T.AsUType Notes t
pnNotes) RootAnn
pnRootAnn

mkSomeParamType :: U.ParameterType -> Either TcTypeError SomeParamType
mkSomeParamType :: ParameterType -> Either TcTypeError SomeParamType
mkSomeParamType (U.ParameterType (T.AsUType (Notes t
notescp :: T.Notes t)) RootAnn
ann) = do
  Dict (ParameterScope t)
T.Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
T.checkScope @(T.ParameterScope t)
    Either BadTypeForScope (Dict (ParameterScope t))
-> (Either BadTypeForScope (Dict (ParameterScope t))
    -> Either TcTypeError (Dict (ParameterScope t)))
-> Either TcTypeError (Dict (ParameterScope t))
forall a b. a -> (a -> b) -> b
& (BadTypeForScope -> TcTypeError)
-> Either BadTypeForScope (Dict (ParameterScope t))
-> Either TcTypeError (Dict (ParameterScope t))
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (T -> BadTypeForScope -> TcTypeError
UnsupportedTypeForScope (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @t))
  ParamNotes t
paramNotes <- Notes t -> RootAnn -> Either ParamEpError (ParamNotes t)
forall (t :: T).
Notes t -> RootAnn -> Either ParamEpError (ParamNotes t)
T.mkParamNotes Notes t
notescp RootAnn
ann
    Either ParamEpError (ParamNotes t)
-> (Either ParamEpError (ParamNotes t)
    -> Either TcTypeError (ParamNotes t))
-> Either TcTypeError (ParamNotes t)
forall a b. a -> (a -> b) -> b
& (ParamEpError -> TcTypeError)
-> Either ParamEpError (ParamNotes t)
-> Either TcTypeError (ParamNotes t)
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ParamEpError -> TcTypeError
IllegalParamDecl
  return $ ParamNotes t -> SomeParamType
forall (t :: T). ParameterScope t => ParamNotes t -> SomeParamType
SomeParamType ParamNotes t
paramNotes

type TcOriginatedContracts = Map ContractHash SomeParamType

-- | Typechecking mode that tells the type checker whether it is typechecking
-- contract code in actual contract, lambda, or test.
data TypeCheckMode op
  = TypeCheckValue
    -- ^ We're typechecking a value.
      (U.Value' [] op, T.T)
      (Maybe BigMapFinder)
      -- ^ When this is a `Just`, we simulate the typechecking behavior of the RPC's @/run_code@ endpoint.
      --
      -- If an integer is found where a big_map is expected,
      -- we use 'BigMapFinder' to check if a big_map exists with that ID.
      -- If it does, and if the big_map's value and key have the expected types, we replace the
      -- big_map ID with the corresponding big_map value.
  | TypeCheckContract SomeParamType
    -- ^ We're typechecking a contract.
  | TypeCheckTest
    -- ^ We're typechecking a set of instructions in a "test" environment like a REPL,
    -- where the instruction @SELF@ would not make sense.

-- | The typechecking state
data TypeCheckEnv op = TypeCheckEnv
  { forall op. TypeCheckEnv op -> TypeCheckMode op
tcMode :: ~(TypeCheckMode op)
  }

type BigMapFinder = Natural -> Maybe SomeVBigMap

data TypeCheckOptions = TypeCheckOptions
  { TypeCheckOptions -> Bool
tcVerbose :: Bool
    -- ^ Whether to add stack type comments after every
    -- instruction a la @octez-client@.
  , TypeCheckOptions -> Bool
tcStrict :: Bool
    -- ^ Whether should we behave like in test run or real run
    -- (real run is more strict).
    --
    -- @octez-client run@'s behaviour can slightly differ from the behaviour
    -- of @octez-client originate@ and @octez-client transfer@. For instance,
    -- some values can be "forged" in test run, but not in a real one,
    -- see: Note [Tickets forging].
    --
    -- Set this to @True@ when need to match the behaviour in the network,
    -- and to @False@ if you prefer providing the user with some convenient
    -- features.
  }

instance Default TypeCheckOptions where
  def :: TypeCheckOptions
def = TypeCheckOptions{ tcVerbose :: Bool
tcVerbose = Bool
False, tcStrict :: Bool
tcStrict = Bool
True }

data TypeCheckInstrEnv = TypeCheckInstrEnv
  { TypeCheckInstrEnv -> ErrorSrcPos
_tcieErrorPos :: ErrorSrcPos
  , TypeCheckInstrEnv -> Maybe (Dict IsNotInView)
_tcieNotInView :: Maybe (Dict T.IsNotInView)
  }

makeLensesWith postfixLFields ''TypeCheckEnv
makeLenses ''TypeCheckInstrEnv

runTypeCheck :: TypeCheckMode op -> TypeCheck op a -> TypeCheckResult op a
runTypeCheck :: forall op a.
TypeCheckMode op -> TypeCheck op a -> TypeCheckResult op a
runTypeCheck = TypeCheckEnv op
-> ReaderT
     (TypeCheckEnv op)
     (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity))
     a
-> ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity) a
forall r (m :: * -> *) a. r -> ReaderT r m a -> m a
usingReaderT (TypeCheckEnv op
 -> ReaderT
      (TypeCheckEnv op)
      (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity))
      a
 -> ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity) a)
-> (TypeCheckMode op -> TypeCheckEnv op)
-> TypeCheckMode op
-> ReaderT
     (TypeCheckEnv op)
     (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity))
     a
-> ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeCheckMode op -> TypeCheckEnv op
forall op. TypeCheckMode op -> TypeCheckEnv op
TypeCheckEnv

-- | Run type checker as if it worked isolated from other world -
-- no access to environment of the current contract is allowed.
--
-- Use this function for test purposes only or for some utilities when
-- environment does not matter. In particular, it is assumed that
-- whatever we typecheck does not depend on the parameter type of the
-- contract which is being typechecked (because there is no contract
-- that we are typechecking).
runTypeCheckIsolated :: TypeCheck op (SomeTcInstr t) -> TypeCheckResult op (SomeTcInstr t)
runTypeCheckIsolated :: forall op (t :: [T]).
TypeCheck op (SomeTcInstr t) -> TypeCheckResult op (SomeTcInstr t)
runTypeCheckIsolated = TypeCheckMode op
-> MultiReaderT (TCEnvs op) (Except (TcError' op)) (SomeTcInstr t)
-> ReaderT TypeCheckOptions (Except (TcError' op)) (SomeTcInstr t)
forall op a.
TypeCheckMode op -> TypeCheck op a -> TypeCheckResult op a
runTypeCheck TypeCheckMode op
forall op. TypeCheckMode op
TypeCheckTest

typeCheckingWith :: TypeCheckOptions -> TypeCheckResult op a -> Either (TcError' op) a
typeCheckingWith :: forall op a.
TypeCheckOptions -> TypeCheckResult op a -> Either (TcError' op) a
typeCheckingWith TypeCheckOptions
options = Except (TcError' op) a -> Either (TcError' op) a
forall e a. Except e a -> Either e a
runExcept (Except (TcError' op) a -> Either (TcError' op) a)
-> (TypeCheckResult op a -> Except (TcError' op) a)
-> TypeCheckResult op a
-> Either (TcError' op) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeCheckOptions -> TypeCheckResult op a -> Except (TcError' op) a
forall r (m :: * -> *) a. r -> ReaderT r m a -> m a
usingReaderT TypeCheckOptions
options

instance Default TypeCheckInstrEnv where
  def :: TypeCheckInstrEnv
def = ErrorSrcPos -> Maybe (Dict IsNotInView) -> TypeCheckInstrEnv
TypeCheckInstrEnv ErrorSrcPos
forall a. Default a => a
def Maybe (Dict IsNotInView)
forall a. Maybe a
Nothing

liftNoExcept
  :: forall m e (a :: Type). MonadMultiReaderT m Identity
  => m a
  -> ChangeMultiReaderBase m (Except e) a
liftNoExcept :: forall (m :: * -> *) e a.
MonadMultiReaderT m Identity =>
m a -> ChangeMultiReaderBase m (Except e) a
liftNoExcept m a
action = (Identity a -> ExceptT e Identity a)
-> m a -> MultiReaderT (MultiReaderIso m) (ExceptT e Identity) a
forall (xs :: [*]) (m' :: * -> *) (m :: * -> *) (n' :: * -> *)
       (n :: * -> *) a b.
(MonadMultiReaderMap xs, m' ~ MultiReaderT xs m,
 n' ~ MultiReaderT xs n, xs ~ MultiReaderIso m') =>
(m a -> n b) -> m' a -> n' b
forall (m' :: * -> *) (m :: * -> *) (n' :: * -> *) (n :: * -> *) a
       b.
(m' ~ MultiReaderT (MultiReaderIso m) m,
 n' ~ MultiReaderT (MultiReaderIso m) n,
 MultiReaderIso m ~ MultiReaderIso m') =>
(m a -> n b) -> m' a -> n' b
mapMultiReaderT (forall (f :: * -> *) a. Applicative f => a -> f a
pure @(Except e) (a -> ExceptT e Identity a)
-> (Identity a -> a) -> Identity a -> ExceptT e Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity a -> a
forall a. Identity a -> a
runIdentity) m a
action

throwingTcError
  :: forall op inp m m'.
     ( MonadMultiReaderT m Identity
     , m' ~ ChangeMultiReaderBase m (Except (TcError' op))
     , MonadError (TcError' op) m'
     )
  => m (TypeCheckedSeq op inp) -> m' (SomeTcInstr inp)
throwingTcError :: forall op (inp :: [T]) (m :: * -> *) (m' :: * -> *).
(MonadMultiReaderT m Identity,
 m' ~ ChangeMultiReaderBase m (Except (TcError' op)),
 MonadError (TcError' op) m') =>
m (TypeCheckedSeq op inp) -> m' (SomeTcInstr inp)
throwingTcError m (TypeCheckedSeq op inp)
action = forall (m :: * -> *) e a.
MonadMultiReaderT m Identity =>
m a -> ChangeMultiReaderBase m (Except e) a
liftNoExcept @_ @(TcError' op) m (TypeCheckedSeq op inp)
action m' (TypeCheckedSeq op inp)
-> (TypeCheckedSeq op inp -> m' (SomeTcInstr inp))
-> m' (SomeTcInstr inp)
forall a b. m' a -> (a -> m' b) -> m' b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([TypeCheckedOp op] -> TcError' op -> m' (SomeTcInstr inp))
-> (SomeTcInstr inp -> m' (SomeTcInstr inp))
-> TypeCheckedSeq op inp
-> m' (SomeTcInstr inp)
forall op a (inp :: [T]).
([TypeCheckedOp op] -> TcError' op -> a)
-> (SomeTcInstr inp -> a) -> TypeCheckedSeq op inp -> a
tcsEither ((TcError' op -> m' (SomeTcInstr inp))
-> [TypeCheckedOp op] -> TcError' op -> m' (SomeTcInstr inp)
forall a b. a -> b -> a
const TcError' op -> m' (SomeTcInstr inp)
forall a. TcError' op -> m' a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError) (SomeTcInstr inp -> m' (SomeTcInstr inp)
forall a. a -> m' a
forall (f :: * -> *) a. Applicative f => a -> f a
pure)

tcEither
  :: (TcError' op -> TypeCheckInstrNoExcept op a) -- ^ Call this if the action throws
  -> (b -> TypeCheckInstrNoExcept op a) -- ^ Call this if it doesn't
  -> TypeCheckInstr op b -- ^ The action to perform
  -> TypeCheckInstrNoExcept op a -- ^ A non-throwing action
tcEither :: forall op a b.
(TcError' op -> TypeCheckInstrNoExcept op a)
-> (b -> TypeCheckInstrNoExcept op a)
-> TypeCheckInstr op b
-> TypeCheckInstrNoExcept op a
tcEither TcError' op -> TypeCheckInstrNoExcept op a
onErr b -> TypeCheckInstrNoExcept op a
onOk TypeCheckInstr op b
action = (TcError' op
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
      a)
-> (b
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
         a)
-> Either (TcError' op) b
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     a
TcError' op -> TypeCheckInstrNoExcept op a
onErr b
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     a
b -> TypeCheckInstrNoExcept op a
onOk (Either (TcError' op) b
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
      a)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (Either (TcError' op) b)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (ExceptT (TcError' op) Identity b
 -> Identity (Either (TcError' op) b))
-> TypeCheckInstr op b
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (Either (TcError' op) b)
forall (xs :: [*]) (m' :: * -> *) (m :: * -> *) (n' :: * -> *)
       (n :: * -> *) a b.
(MonadMultiReaderMap xs, m' ~ MultiReaderT xs m,
 n' ~ MultiReaderT xs n, xs ~ MultiReaderIso m') =>
(m a -> n b) -> m' a -> n' b
forall (m' :: * -> *) (m :: * -> *) (n' :: * -> *) (n :: * -> *) a
       b.
(m'
 ~ MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions] m,
 n'
 ~ MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions] n,
 '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
 ~ MultiReaderIso m') =>
(m a -> n b) -> m' a -> n' b
mapMultiReaderT (Either (TcError' op) b -> Identity (Either (TcError' op) b)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (TcError' op) b -> Identity (Either (TcError' op) b))
-> (ExceptT (TcError' op) Identity b -> Either (TcError' op) b)
-> ExceptT (TcError' op) Identity b
-> Identity (Either (TcError' op) b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT (TcError' op) Identity b -> Either (TcError' op) b
forall e a. Except e a -> Either e a
runExcept) TypeCheckInstr op b
action

-- | Operation types that appear in @AbstractInstr@.
--
-- 'Data' superclass constraint is used to search for particular sub-instructions.
class Data op => IsInstrOp op where
  -- | Lift a single instruction to operation.
  --
  -- This is used only in error messages.
  liftInstr :: U.InstrAbstract [] op -> op

  -- | Get callstack at this instruction, if any given.
  --
  -- This is used only in error messages.
  pickErrorSrcPos :: op -> Maybe ErrorSrcPos

  -- | Do our best to re-interpret an instruction as a value.
  --
  -- For instance, @{ {}, {} }@ may turn out to be represented both as nested
  -- @SeqEx@s and as nested @ValueList@ & @ValueNil@s.
  -- This function, along with 'tryValToOp', let us convert between these
  -- two forms.
  --
  -- TODO [#785]: try to remove these two functions
  tryOpToVal :: op -> Maybe (U.Value' [] op)

  -- | Do our best to re-interpret a value as an instruction.
  --
  -- This does the opposite to 'tryOpToVal'.
  --
  -- If a value is already a lambda, this can return 'Nothing'.
  tryValToOp :: U.Value' [] op -> Maybe op

instance IsInstrOp U.ExpandedOp where
  liftInstr :: InstrAbstract [] ExpandedOp -> ExpandedOp
liftInstr = InstrAbstract [] ExpandedOp -> ExpandedOp
U.PrimEx

  pickErrorSrcPos :: ExpandedOp -> Maybe ErrorSrcPos
pickErrorSrcPos = \case
    U.WithSrcEx ErrorSrcPos
cs ExpandedOp
_ -> ErrorSrcPos -> Maybe ErrorSrcPos
forall a. a -> Maybe a
Just ErrorSrcPos
cs
    ExpandedOp
_ -> Maybe ErrorSrcPos
forall a. Maybe a
Nothing

  tryOpToVal :: ExpandedOp -> Maybe (Value' [] ExpandedOp)
tryOpToVal = \case
    U.SeqEx []      -> Value' [] ExpandedOp -> Maybe (Value' [] ExpandedOp)
forall a. a -> Maybe a
Just Value' [] ExpandedOp
forall {k} (f :: k -> *) (op :: k). Value' f op
U.ValueNil
    U.SeqEx [ExpandedOp]
xs      -> (NonEmpty $ Value' [] ExpandedOp) -> Value' [] ExpandedOp
forall {k} (f :: k -> *) (op :: k).
(NonEmpty $ Value' f op) -> Value' f op
U.ValueSeq ((NonEmpty $ Value' [] ExpandedOp) -> Value' [] ExpandedOp)
-> ([Value' [] ExpandedOp] -> NonEmpty $ Value' [] ExpandedOp)
-> [Value' [] ExpandedOp]
-> Value' [] ExpandedOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ListElement (NonEmpty $ Value' [] ExpandedOp)]
-> NonEmpty $ Value' [] ExpandedOp
[Value' [] ExpandedOp] -> NonEmpty $ Value' [] ExpandedOp
forall l. (FromList l, FromListC l) => [ListElement l] -> l
fromList ([Value' [] ExpandedOp] -> Value' [] ExpandedOp)
-> Maybe [Value' [] ExpandedOp] -> Maybe (Value' [] ExpandedOp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ExpandedOp -> Maybe (Value' [] ExpandedOp))
-> [ExpandedOp] -> Maybe [Value' [] ExpandedOp]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ExpandedOp -> Maybe (Value' [] ExpandedOp)
forall op. IsInstrOp op => op -> Maybe (Value' [] op)
tryOpToVal [ExpandedOp]
xs
    U.PrimEx {}     -> Maybe (Value' [] ExpandedOp)
forall a. Maybe a
Nothing
    U.WithSrcEx ErrorSrcPos
_ ExpandedOp
i -> ExpandedOp -> Maybe (Value' [] ExpandedOp)
forall op. IsInstrOp op => op -> Maybe (Value' [] op)
tryOpToVal ExpandedOp
i

  tryValToOp :: Value' [] ExpandedOp -> Maybe ExpandedOp
tryValToOp = \case
    Value' [] ExpandedOp
U.ValueNil      -> ExpandedOp -> Maybe ExpandedOp
forall a. a -> Maybe a
Just (ExpandedOp -> Maybe ExpandedOp) -> ExpandedOp -> Maybe ExpandedOp
forall a b. (a -> b) -> a -> b
$ [ExpandedOp] -> ExpandedOp
U.SeqEx []
    U.ValueSeq NonEmpty $ Value' [] ExpandedOp
xs   -> [ExpandedOp] -> ExpandedOp
U.SeqEx ([ExpandedOp] -> ExpandedOp)
-> (NonEmpty ExpandedOp -> [ExpandedOp])
-> NonEmpty ExpandedOp
-> ExpandedOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty ExpandedOp -> [Element (NonEmpty ExpandedOp)]
NonEmpty ExpandedOp -> [ExpandedOp]
forall t. Container t => t -> [Element t]
toList (NonEmpty ExpandedOp -> ExpandedOp)
-> Maybe (NonEmpty ExpandedOp) -> Maybe ExpandedOp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value' [] ExpandedOp -> Maybe ExpandedOp)
-> (NonEmpty $ Value' [] ExpandedOp) -> Maybe (NonEmpty ExpandedOp)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse Value' [] ExpandedOp -> Maybe ExpandedOp
forall op. IsInstrOp op => Value' [] op -> Maybe op
tryValToOp NonEmpty $ Value' [] ExpandedOp
xs
    Value' [] ExpandedOp
_               -> Maybe ExpandedOp
forall a. Maybe a
Nothing

-- | Perform a throwing action on an acquired instruction. Preserve the acquired
-- result by embedding it into a type checking tree with a specified parent
-- instruction.
preserving
  :: TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
  -- ^ Acquiring computation
  -> ([TypeCheckedOp op] -> TypeCheckedInstr op)
  -- ^ The parent instruction constructor
  -> (SomeTcInstr inp -> TypeCheckInstr op (SomeTcInstr inp'))
  -- ^ The throwing action
  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
preserving :: forall op (inp :: [T]) (inp' :: [T]).
TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
-> ([TypeCheckedOp op] -> TypeCheckedInstr op)
-> (SomeTcInstr inp -> TypeCheckInstr op (SomeTcInstr inp'))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
preserving TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
acquire [TypeCheckedOp op] -> TypeCheckedInstr op
con SomeTcInstr inp -> TypeCheckInstr op (SomeTcInstr inp')
action = TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
-> ([TypeCheckedOp op] -> TypeCheckedInstr op)
-> (SomeTcInstr inp
    -> MultiReaderT (TCInstrEnvs op) Identity (TypeCheckedSeq op inp'))
-> MultiReaderT (TCInstrEnvs op) Identity (TypeCheckedSeq op inp')
forall op (inp :: [T]) (inp' :: [T]).
TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
-> ([TypeCheckedOp op] -> TypeCheckedInstr op)
-> (SomeTcInstr inp
    -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp'))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
preserving' TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
acquire [TypeCheckedOp op] -> TypeCheckedInstr op
con
  (\SomeTcInstr inp
instr -> SomeTcInstr inp -> TypeCheckInstr op (SomeTcInstr inp')
action SomeTcInstr inp
instr ReaderT
  TypeCheckInstrEnv
  (ReaderT
     (TypeCheckEnv op)
     (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
  (SomeTcInstr inp')
-> (ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (SomeTcInstr inp')
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
         (TypeCheckedSeq op inp'))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp')
forall a b. a -> (a -> b) -> b
& (TcError' op
 -> MultiReaderT (TCInstrEnvs op) Identity (TypeCheckedSeq op inp'))
-> (SomeTcInstr inp'
    -> MultiReaderT (TCInstrEnvs op) Identity (TypeCheckedSeq op inp'))
-> TypeCheckInstr op (SomeTcInstr inp')
-> MultiReaderT (TCInstrEnvs op) Identity (TypeCheckedSeq op inp')
forall op a b.
(TcError' op -> TypeCheckInstrNoExcept op a)
-> (b -> TypeCheckInstrNoExcept op a)
-> TypeCheckInstr op b
-> TypeCheckInstrNoExcept op a
tcEither
    (\TcError' op
err -> TypeCheckedSeq op inp'
-> MultiReaderT (TCInstrEnvs op) Identity (TypeCheckedSeq op inp')
forall a. a -> MultiReaderT (TCInstrEnvs op) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq op inp'
 -> MultiReaderT (TCInstrEnvs op) Identity (TypeCheckedSeq op inp'))
-> TypeCheckedSeq op inp'
-> MultiReaderT (TCInstrEnvs op) Identity (TypeCheckedSeq op inp')
forall a b. (a -> b) -> a -> b
$ TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp'
forall op (inp :: [T]).
TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
IllTypedSeq TcError' op
err [TypeCheckedInstr op -> IllTypedInstr op
forall op. TypeCheckedInstr op -> IllTypedInstr op
SemiTypedInstr (TypeCheckedInstr op -> IllTypedInstr op)
-> TypeCheckedInstr op -> IllTypedInstr op
forall a b. (a -> b) -> a -> b
$ [TypeCheckedOp op] -> TypeCheckedInstr op
con [SomeTcInstr inp -> TypeCheckedOp op
forall (inp :: [T]) op. SomeTcInstr inp -> TypeCheckedOp op
someInstrToOp SomeTcInstr inp
instr]])
    (TypeCheckedSeq op inp'
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp')
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq op inp'
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
      (TypeCheckedSeq op inp'))
-> (SomeTcInstr inp' -> TypeCheckedSeq op inp')
-> SomeTcInstr inp'
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeTcInstr inp' -> TypeCheckedSeq op inp'
forall op (inp :: [T]). SomeTcInstr inp -> TypeCheckedSeq op inp
WellTypedSeq))

-- | Perform a non-throwing action on an acquired instruction. Preserve the
-- acquired result even if the action does not succeed. Embed the result into a
-- type checking tree with a specified parent instruction.
preserving'
  :: TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
  -- ^ Acquiring computation
  -> ([TypeCheckedOp op] -> TypeCheckedInstr op)
  -- ^ The parent instruction constructor
  -> (SomeTcInstr inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp'))
  -- ^ The action
  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
preserving' :: forall op (inp :: [T]) (inp' :: [T]).
TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
-> ([TypeCheckedOp op] -> TypeCheckedInstr op)
-> (SomeTcInstr inp
    -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp'))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
preserving' TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
acquire [TypeCheckedOp op] -> TypeCheckedInstr op
con SomeTcInstr inp
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
action =
  ReaderT
  TypeCheckInstrEnv
  (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
  (TypeCheckedSeq op inp)
TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
acquire ReaderT
  TypeCheckInstrEnv
  (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
  (TypeCheckedSeq op inp)
-> (TypeCheckedSeq op inp
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
         (TypeCheckedSeq op inp'))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp')
forall a b.
ReaderT
  TypeCheckInstrEnv
  (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
  a
-> (a
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
         b)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([TypeCheckedOp op]
 -> TcError' op
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
      (TypeCheckedSeq op inp'))
-> (SomeTcInstr inp
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
         (TypeCheckedSeq op inp'))
-> TypeCheckedSeq op inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp')
forall op a (inp :: [T]).
([TypeCheckedOp op] -> TcError' op -> a)
-> (SomeTcInstr inp -> a) -> TypeCheckedSeq op inp -> a
tcsEither
    (\[TypeCheckedOp op]
tcOps TcError' op
err -> TypeCheckedSeq op inp'
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp')
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq op inp'
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
      (TypeCheckedSeq op inp'))
-> TypeCheckedSeq op inp'
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp')
forall a b. (a -> b) -> a -> b
$ TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp'
forall op (inp :: [T]).
TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
IllTypedSeq TcError' op
err [TypeCheckedInstr op -> IllTypedInstr op
forall op. TypeCheckedInstr op -> IllTypedInstr op
SemiTypedInstr (TypeCheckedInstr op -> IllTypedInstr op)
-> TypeCheckedInstr op -> IllTypedInstr op
forall a b. (a -> b) -> a -> b
$ [TypeCheckedOp op] -> TypeCheckedInstr op
con [TypeCheckedOp op]
tcOps])
    (SomeTcInstr inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp')
SomeTcInstr inp
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp')
action)

-- | Acquire a resource. If successfully, call a follow-up action on it,
-- otherwise embed the error into a type checking tree along with a specified
-- untyped instruction.
guarding
  :: IsInstrOp op
  => U.InstrAbstract [] op -- ^ Untyped instruction
  -> TypeCheckInstr op a -- ^ Acquiring computation
  -> (a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)) -- ^ Follow-up action
  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
guarding :: forall op a (inp :: [T]).
IsInstrOp op =>
InstrAbstract [] op
-> TypeCheckInstr op a
-> (a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
guarding InstrAbstract [] op
instr TypeCheckInstr op a
cond a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
action = do
  ReaderT
  TypeCheckInstrEnv
  (ReaderT
     (TypeCheckEnv op)
     (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
  a
TypeCheckInstr op a
cond ReaderT
  TypeCheckInstrEnv
  (ReaderT
     (TypeCheckEnv op)
     (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
  a
-> (ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      a
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
         (TypeCheckedSeq op inp))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp)
forall a b. a -> (a -> b) -> b
& (TcError' op -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> (a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> TypeCheckInstr op a
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
forall op a b.
(TcError' op -> TypeCheckInstrNoExcept op a)
-> (b -> TypeCheckInstrNoExcept op a)
-> TypeCheckInstr op b
-> TypeCheckInstrNoExcept op a
tcEither
    (\TcError' op
err -> TypeCheckedSeq op inp
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
forall a. a -> MultiReaderT (TCInstrEnvs op) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeCheckedSeq op inp
 -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> TypeCheckedSeq op inp
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
forall a b. (a -> b) -> a -> b
$ TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
forall op (inp :: [T]).
TcError' op -> [IllTypedInstr op] -> TypeCheckedSeq op inp
IllTypedSeq TcError' op
err [op -> IllTypedInstr op
forall op. op -> IllTypedInstr op
NonTypedInstr (op -> IllTypedInstr op) -> op -> IllTypedInstr op
forall a b. (a -> b) -> a -> b
$ InstrAbstract [] op -> op
forall op. IsInstrOp op => InstrAbstract [] op -> op
liftInstr InstrAbstract [] op
instr])
    (a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
action)

-- | Same as @guarding@ but doesn't pass an acquired result to a follow-up
-- action.
guarding_
  :: IsInstrOp op
  => U.InstrAbstract [] op
  -> TypeCheckInstr op a
  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
guarding_ :: forall op a (inp :: [T]).
IsInstrOp op =>
InstrAbstract [] op
-> TypeCheckInstr op a
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
guarding_ InstrAbstract [] op
instr TypeCheckInstr op a
cond TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
action = InstrAbstract [] op
-> TypeCheckInstr op a
-> (a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
forall op a (inp :: [T]).
IsInstrOp op =>
InstrAbstract [] op
-> TypeCheckInstr op a
-> (a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
guarding InstrAbstract [] op
instr TypeCheckInstr op a
cond (ReaderT
  TypeCheckInstrEnv
  (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
  (TypeCheckedSeq op inp)
-> a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp)
forall a b. a -> b -> a
const ReaderT
  TypeCheckInstrEnv
  (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
  (TypeCheckedSeq op inp)
TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
action)

-- | Some type checker function.
--
-- It accepts untyped instructions to typecheck as @instr@ value, and @op@ type
-- stands for the basic operation type like @ExpandedOp@.
type TcInstr op instr
   = forall inp. (T.SingI inp)
      => instr
      -> HST inp
      -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)

-- | Type checker function for the operation like @ExpandedOp@.
-- Function of this type we carry in most of the other functions to let
-- them recurse.
type TcInstrBase op = TcInstr op op