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

-- | This module provides a data type for representing a partially typed
-- sequence of instructions.
--
-- It is needed to represent the fact that there can only be one well-typed node
-- in a sequence and it is the first one. Also, it serves its role to remove
-- @TcError@ usage from @TypeCheckedOp@.
module Morley.Michelson.TypeCheck.TypeCheckedSeq
  ( TypeCheckedInstr
  , TypeCheckedOp(..)
  , IllTypedInstr(..)
  , TypeCheckedSeq(..)
  , tcsEither
  , seqToOps
  , someInstrToOp
  , someViewToOp
  ) where

import Morley.Michelson.TypeCheck.Error (TcError')
import Morley.Michelson.TypeCheck.TypeCheckedOp
  (IllTypedInstr(..), TypeCheckedInstr, TypeCheckedOp(..), someInstrToOp, someViewToOp)
import Morley.Michelson.TypeCheck.Types (SomeTcInstr(..))

-- | Represents a partiall typed sequence of instructions.
data TypeCheckedSeq op inp
  -- | A fully well-typed sequence.
  = WellTypedSeq (SomeTcInstr inp)
  -- | A well-typed prefix followed by some error and semi-typed instructions.
  | MixedSeq (SomeTcInstr inp) (TcError' op) [IllTypedInstr op]
  -- | There is no well-typed prefix, only an error and semi-typed instructions.
  | IllTypedSeq (TcError' op) [IllTypedInstr op]

seqToOps :: TypeCheckedSeq op inp -> [TypeCheckedOp op]
seqToOps :: forall op (inp :: [T]). TypeCheckedSeq op inp -> [TypeCheckedOp op]
seqToOps = \case
  WellTypedSeq SomeTcInstr inp
instr -> [SomeTcInstr inp -> TypeCheckedOp op
forall (inp :: [T]) op. SomeTcInstr inp -> TypeCheckedOp op
someInstrToOp SomeTcInstr inp
instr]
  MixedSeq SomeTcInstr inp
instr TcError' op
_ [IllTypedInstr op]
tail' -> SomeTcInstr inp -> TypeCheckedOp op
forall (inp :: [T]) op. SomeTcInstr inp -> TypeCheckedOp op
someInstrToOp SomeTcInstr inp
instr TypeCheckedOp op -> [TypeCheckedOp op] -> [TypeCheckedOp op]
forall a. a -> [a] -> [a]
: (IllTypedInstr op -> TypeCheckedOp op)
-> [IllTypedInstr op] -> [TypeCheckedOp op]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map IllTypedInstr op -> TypeCheckedOp op
forall op. IllTypedInstr op -> TypeCheckedOp op
IllTypedOp [IllTypedInstr op]
tail'
  IllTypedSeq TcError' op
_ [IllTypedInstr op]
tail' -> (IllTypedInstr op -> TypeCheckedOp op)
-> [IllTypedInstr op] -> [TypeCheckedOp op]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map IllTypedInstr op -> TypeCheckedOp op
forall op. IllTypedInstr op -> TypeCheckedOp op
IllTypedOp [IllTypedInstr op]
tail'

-- | Case analysis for @TypeCheckedSeq@.
tcsEither
  :: ([TypeCheckedOp op] -> TcError' op -> a)
     -- ^ On error, with all already typechecked operations
  -> (SomeTcInstr inp -> a) -- ^ On well-typed instruction
  -> TypeCheckedSeq op inp -- ^ The sequence to dispatch on
  -> a
tcsEither :: forall op a (inp :: [T]).
([TypeCheckedOp op] -> TcError' op -> a)
-> (SomeTcInstr inp -> a) -> TypeCheckedSeq op inp -> a
tcsEither [TypeCheckedOp op] -> TcError' op -> a
onErr SomeTcInstr inp -> a
onInstr TypeCheckedSeq op inp
v = case TypeCheckedSeq op inp
v of
  WellTypedSeq SomeTcInstr inp
instr -> SomeTcInstr inp -> a
onInstr SomeTcInstr inp
instr
  MixedSeq SomeTcInstr inp
_ TcError' op
err [IllTypedInstr op]
_ -> [TypeCheckedOp op] -> TcError' op -> a
onErr (TypeCheckedSeq op inp -> [TypeCheckedOp op]
forall op (inp :: [T]). TypeCheckedSeq op inp -> [TypeCheckedOp op]
seqToOps TypeCheckedSeq op inp
v) TcError' op
err
  IllTypedSeq TcError' op
err [IllTypedInstr op]
_ -> [TypeCheckedOp op] -> TcError' op -> a
onErr (TypeCheckedSeq op inp -> [TypeCheckedOp op]
forall op (inp :: [T]). TypeCheckedSeq op inp -> [TypeCheckedOp op]
seqToOps TypeCheckedSeq op inp
v) TcError' op
err