module Morley.Michelson.TypeCheck.TypeCheckedSeq
( TypeCheckedInstr
, TypeCheckedOp(..)
, IllTypedInstr(..)
, TypeCheckedSeq(..)
, Nesting
, tcsEither
, seqToOps
, someInstrToOp
, someViewToOp
) where
import Morley.Michelson.TypeCheck.Error (TcError')
import Morley.Michelson.TypeCheck.TypeCheckedOp
import Morley.Michelson.TypeCheck.Types (SomeTcInstr(..))
data TypeCheckedSeq op inp
= WellTypedSeq (SomeTcInstr inp)
| MixedSeq Nesting (SomeTcInstr inp) (TcError' op) [IllTypedInstr op]
| 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 Nesting
nesting SomeTcInstr inp
instr TcError' op
_ [IllTypedInstr op]
tail' -> [SomeTcInstr inp
-> (forall (out :: [T]).
(SingI inp, SingI out) =>
Instr inp out -> [IllTypedInstr op] -> TypeCheckedOp op)
-> [IllTypedInstr op]
-> TypeCheckedOp op
forall (inp :: [T]) r.
SomeTcInstr inp
-> (forall (out :: [T]).
(SingI inp, SingI out) =>
Instr inp out -> r)
-> r
withSomeTcInstr SomeTcInstr inp
instr (Nesting -> SomeSingInstr -> [IllTypedInstr op] -> TypeCheckedOp op
forall op.
Nesting -> SomeSingInstr -> [IllTypedInstr op] -> TypeCheckedOp op
MixedOp Nesting
nesting (SomeSingInstr -> [IllTypedInstr op] -> TypeCheckedOp op)
-> (Instr inp out -> SomeSingInstr)
-> Instr inp out
-> [IllTypedInstr op]
-> TypeCheckedOp op
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr inp out -> SomeSingInstr
forall (inp :: [T]) (out :: [T]).
(SingI inp, SingI out) =>
Instr inp out -> SomeSingInstr
SomeSingInstr) [IllTypedInstr op]
tail']
IllTypedSeq TcError' op
_ [IllTypedInstr op]
tail' -> [[IllTypedInstr op] -> TypeCheckedOp op
forall op. [IllTypedInstr op] -> TypeCheckedOp op
IllTypedOp [IllTypedInstr op]
tail']
tcsEither
:: ([TypeCheckedOp op] -> TcError' op -> a)
-> (SomeTcInstr inp -> a)
-> TypeCheckedSeq op inp
-> 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 Nesting
_ 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