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

-- | 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 Michelson.TypeCheck.TypeCheckedSeq
  ( TypeCheckedInstr
  , TypeCheckedOp(..)
  , IllTypedInstr(..)
  , TypeCheckedSeq(..)
  , tcsEither
  , seqToOps
  , someInstrToOp
  ) where

import Michelson.TypeCheck.Error (TCError)
import Michelson.TypeCheck.TypeCheckedOp
  (IllTypedInstr(..), TypeCheckedInstr, TypeCheckedOp(..), someInstrToOp)
import Michelson.TypeCheck.Types (SomeInstr(..))

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

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

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