{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
module Morley.Michelson.FailPattern
( TypicalFailWith
, typicalFailWithTag
, isTypicalFailWith
, modifyTypicalFailWith
) where
import Data.Singletons (withSingI)
import Morley.Michelson.Text (MText)
import Morley.Michelson.Typed
data TypicalFailWith
= FailWithString MText
| FailWithConstantPair MText SomeConstant
| FailWithStackValue MText
typicalFailWithTag :: TypicalFailWith -> MText
typicalFailWithTag :: TypicalFailWith -> MText
typicalFailWithTag = \case
FailWithString MText
str -> MText
str
FailWithConstantPair MText
str SomeConstant
_ -> MText
str
FailWithStackValue MText
str -> MText
str
isTypicalFailWith :: Instr inp out -> Maybe TypicalFailWith
isTypicalFailWith :: forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe TypicalFailWith
isTypicalFailWith = \case
Seq Instr inp b
i1 Instr b out
FAILWITH -> Instr inp (a : s) -> Maybe TypicalFailWith
forall (inp :: [T]) (a :: T) (out :: [T]).
Instr inp (a : out) -> Maybe TypicalFailWith
isTypicalPreFailWith Instr inp b
Instr inp (a : s)
i1
Instr inp out
_ -> Maybe TypicalFailWith
forall a. Maybe a
Nothing
where
isTypicalPreFailWith ::
Instr inp (a ': out) -> Maybe TypicalFailWith
isTypicalPreFailWith :: forall (inp :: [T]) (a :: T) (out :: [T]).
Instr inp (a : out) -> Maybe TypicalFailWith
isTypicalPreFailWith =
\case
PUSH Value' Instr t
v -> Value' Instr t -> Maybe TypicalFailWith
forall (t :: T).
ConstantScope t =>
Value t -> Maybe TypicalFailWith
isTypicalErrorConstant Value' Instr t
v
Seq Instr inp b
_ (PUSH Value' Instr t
v) -> Value' Instr t -> Maybe TypicalFailWith
forall (t :: T).
ConstantScope t =>
Value t -> Maybe TypicalFailWith
isTypicalErrorConstant Value' Instr t
v
Seq (PUSH Value' Instr t
v) PAIR{} -> MText -> TypicalFailWith
FailWithStackValue (MText -> TypicalFailWith) -> Maybe MText -> Maybe TypicalFailWith
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value' Instr t -> Maybe MText
forall (t :: T). Value t -> Maybe MText
isStringValue Value' Instr t
v
Seq (Seq Instr inp b
_ (PUSH Value' Instr t
v)) PAIR{} -> MText -> TypicalFailWith
FailWithStackValue (MText -> TypicalFailWith) -> Maybe MText -> Maybe TypicalFailWith
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value' Instr t -> Maybe MText
forall (t :: T). Value t -> Maybe MText
isStringValue Value' Instr t
v
Instr inp (a : out)
_ -> Maybe TypicalFailWith
forall a. Maybe a
Nothing
isTypicalErrorConstant ::
forall t. ConstantScope t => Value t -> Maybe TypicalFailWith
isTypicalErrorConstant :: forall (t :: T).
ConstantScope t =>
Value t -> Maybe TypicalFailWith
isTypicalErrorConstant Value t
v
| Just MText
str <- Value t -> Maybe MText
forall (t :: T). Value t -> Maybe MText
isStringValue Value t
v = TypicalFailWith -> Maybe TypicalFailWith
forall a. a -> Maybe a
Just (MText -> TypicalFailWith
FailWithString MText
str)
| VPair (VString MText
str, Value' Instr r
secondItem) <- Value t
v =
case forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @t of
STPair Sing n1
l Sing n2
r -> Sing 'TString
-> (SingI 'TString => Maybe TypicalFailWith)
-> Maybe TypicalFailWith
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
Sing 'TString
l ((SingI 'TString => Maybe TypicalFailWith)
-> Maybe TypicalFailWith)
-> (SingI 'TString => Maybe TypicalFailWith)
-> Maybe TypicalFailWith
forall a b. (a -> b) -> a -> b
$ Sing r
-> (SingI r => Maybe TypicalFailWith) -> Maybe TypicalFailWith
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing r
Sing n2
r ((SingI r => Maybe TypicalFailWith) -> Maybe TypicalFailWith)
-> (SingI r => Maybe TypicalFailWith) -> Maybe TypicalFailWith
forall a b. (a -> b) -> a -> b
$ TypicalFailWith -> Maybe TypicalFailWith
forall a. a -> Maybe a
Just (MText -> SomeConstant -> TypicalFailWith
FailWithConstantPair MText
str (Value' Instr r -> SomeConstant
forall (t :: T). ConstantScope t => Value t -> SomeConstant
SomeConstant Value' Instr r
secondItem))
| Bool
otherwise = Maybe TypicalFailWith
forall a. Maybe a
Nothing
modifyTypicalFailWith
:: HasCallStack
=> (MText -> SomeConstant)
-> Instr inp out
-> Instr inp out
modifyTypicalFailWith :: forall (inp :: [T]) (out :: [T]).
HasCallStack =>
(MText -> SomeConstant) -> Instr inp out -> Instr inp out
modifyTypicalFailWith MText -> SomeConstant
f = Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
Instr inp out -> Instr inp out
modifyTypicalFailWith' (Instr inp out -> Instr inp out)
-> (Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
linearizeLeft
where
modifyTypicalFailWith' :: HasCallStack => Instr inp out -> Instr inp out
modifyTypicalFailWith' :: forall (inp :: [T]) (out :: [T]).
HasCallStack =>
Instr inp out -> Instr inp out
modifyTypicalFailWith' =
\case
Seq Instr inp b
i1 Instr b out
FAILWITH ->
case Instr inp b
i1 of
PUSH Value' Instr t
v -> Value' Instr t -> Instr inp out
forall (v :: T) (inp :: [T]) (out :: [T]).
(HasCallStack, ConstantScope v) =>
Value v -> Instr inp out
onPush Value' Instr t
v
Seq Instr inp b
i0 (PUSH Value' Instr t
v) -> Instr inp b -> Instr b out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr inp b
i0 (Value' Instr t -> Instr b out
forall (v :: T) (inp :: [T]) (out :: [T]).
(HasCallStack, ConstantScope v) =>
Value v -> Instr inp out
onPush Value' Instr t
v)
Seq (AnnPUSH ann :: Anns '[VarAnn, Notes t]
ann@(Anns2' VarAnn
s Notes t
_) Value' Instr t
v) (AnnPAIR Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
ann')
| Value' Instr t
_ :: Value a <- Value' Instr t
v
, Instr (b : s) ('TPair t b : s)
_ :: Instr (b ': s) ('TPair a b ': s) <- Instr inp b
i1 ->
case forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @('TPair a b) of
STPair Sing n1
l Sing n2
r -> Sing t -> (SingI t => Instr inp out) -> Instr inp out
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing t
Sing n1
l ((SingI t => Instr inp out) -> Instr inp out)
-> (SingI t => Instr inp out) -> Instr inp out
forall a b. (a -> b) -> a -> b
$ Sing b -> (SingI b => Instr inp out) -> Instr inp out
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing b
Sing n2
r ((SingI b => Instr inp out) -> Instr inp out)
-> (SingI b => Instr inp out) -> Instr inp out
forall a b. (a -> b) -> a -> b
$ case Value' Instr t -> Maybe MText
forall (t :: T). Value t -> Maybe MText
isStringValue Value' Instr t
v of
Just (MText -> SomeConstant
f -> SomeConstant Value t
v') ->
Anns '[VarAnn, Notes t] -> Value t -> Instr (b : s) (t : b : s)
forall (t :: T) (inp :: [T]).
ConstantScope t =>
Anns '[VarAnn, Notes t] -> Value' Instr t -> Instr inp (t : inp)
AnnPUSH (VarAnn -> Notes t -> Anns '[VarAnn, Notes t]
forall {k} (a :: k) (t :: T).
(Typeable a, SingI t) =>
Annotation a -> Notes t -> Anns '[Annotation a, Notes t]
Anns2' VarAnn
s Notes t
forall (t :: T). SingI t => Notes t
starNotes) Value t
v' Instr (b : s) (t : b : s)
-> Instr (t : b : s) ('TPair t b : s)
-> Instr (b : s) ('TPair t b : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
-> Instr (t : b : s) ('TPair t b : s)
forall (a :: T) (b :: T) (s :: [T]).
Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
-> Instr (a : b : s) ('TPair a b : s)
AnnPAIR Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
ann' Instr (b : s) ('TPair t b : s)
-> Instr ('TPair t b : s) out -> Instr (b : s) out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr ('TPair t b : s) out
forall (a :: T) (s :: [T]) (out :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : s) out
FAILWITH
Maybe MText
Nothing ->
Anns '[VarAnn, Notes t]
-> Value' Instr t -> Instr (b : s) (t : b : s)
forall (t :: T) (inp :: [T]).
ConstantScope t =>
Anns '[VarAnn, Notes t] -> Value' Instr t -> Instr inp (t : inp)
AnnPUSH Anns '[VarAnn, Notes t]
ann Value' Instr t
v Instr (b : s) (t : b : s)
-> Instr (t : b : s) ('TPair t b : s)
-> Instr (b : s) ('TPair t b : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
-> Instr (t : b : s) ('TPair t b : s)
forall (a :: T) (b :: T) (s :: [T]).
Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
-> Instr (a : b : s) ('TPair a b : s)
AnnPAIR Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
ann' Instr (b : s) ('TPair t b : s)
-> Instr ('TPair t b : s) out -> Instr (b : s) out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr ('TPair t b : s) out
forall (a :: T) (s :: [T]) (out :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : s) out
FAILWITH
Seq (Seq Instr inp b
i0 (AnnPUSH ann :: Anns '[VarAnn, Notes t]
ann@(Anns2' VarAnn
s Notes t
_) Value' Instr t
v)) (AnnPAIR Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
ann')
| Value' Instr t
_ :: Value a <- Value' Instr t
v
, Instr inp ('TPair t b : s)
_ :: Instr s0 ('TPair a b ': s) <- Instr inp b
i1 ->
case forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @('TPair a b) of
STPair Sing n1
l Sing n2
r -> Sing t -> (SingI t => Instr inp out) -> Instr inp out
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing t
Sing n1
l ((SingI t => Instr inp out) -> Instr inp out)
-> (SingI t => Instr inp out) -> Instr inp out
forall a b. (a -> b) -> a -> b
$ Sing b -> (SingI b => Instr inp out) -> Instr inp out
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing b
Sing n2
r ((SingI b => Instr inp out) -> Instr inp out)
-> (SingI b => Instr inp out) -> Instr inp out
forall a b. (a -> b) -> a -> b
$ Instr inp b -> Instr b out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr inp b
i0 (Instr b out -> Instr inp out) -> Instr b out -> Instr inp out
forall a b. (a -> b) -> a -> b
$ case Value' Instr t -> Maybe MText
forall (t :: T). Value t -> Maybe MText
isStringValue Value' Instr t
v of
Just (MText -> SomeConstant
f -> SomeConstant Value t
v') ->
Anns '[VarAnn, Notes t] -> Value t -> Instr (b : s) (t : b : s)
forall (t :: T) (inp :: [T]).
ConstantScope t =>
Anns '[VarAnn, Notes t] -> Value' Instr t -> Instr inp (t : inp)
AnnPUSH (VarAnn -> Notes t -> Anns '[VarAnn, Notes t]
forall {k} (a :: k) (t :: T).
(Typeable a, SingI t) =>
Annotation a -> Notes t -> Anns '[Annotation a, Notes t]
Anns2' VarAnn
s Notes t
forall (t :: T). SingI t => Notes t
starNotes) Value t
v' Instr (b : s) (t : b : s)
-> Instr (t : b : s) ('TPair t b : s)
-> Instr (b : s) ('TPair t b : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
-> Instr (t : b : s) ('TPair t b : s)
forall (a :: T) (b :: T) (s :: [T]).
Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
-> Instr (a : b : s) ('TPair a b : s)
AnnPAIR Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
ann' Instr (b : s) ('TPair t b : s)
-> Instr ('TPair t b : s) out -> Instr (b : s) out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr ('TPair t b : s) out
forall (a :: T) (s :: [T]) (out :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : s) out
FAILWITH
Maybe MText
Nothing ->
Anns '[VarAnn, Notes t]
-> Value' Instr t -> Instr (b : s) (t : b : s)
forall (t :: T) (inp :: [T]).
ConstantScope t =>
Anns '[VarAnn, Notes t] -> Value' Instr t -> Instr inp (t : inp)
AnnPUSH Anns '[VarAnn, Notes t]
ann Value' Instr t
v Instr (b : s) (t : b : s)
-> Instr (t : b : s) ('TPair t b : s)
-> Instr (b : s) ('TPair t b : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
-> Instr (t : b : s) ('TPair t b : s)
forall (a :: T) (b :: T) (s :: [T]).
Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
-> Instr (a : b : s) ('TPair a b : s)
AnnPAIR Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
ann' Instr (b : s) ('TPair t b : s)
-> Instr ('TPair t b : s) out -> Instr (b : s) out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr ('TPair t b : s) out
forall (a :: T) (s :: [T]) (out :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : s) out
FAILWITH
Instr inp b
_ -> Instr inp b -> Instr b out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr inp b
i1 Instr b out
forall (a :: T) (s :: [T]) (out :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : s) out
FAILWITH
Instr inp out
i -> Instr inp out
i
onPush ::
(HasCallStack, ConstantScope v) => Value v -> Instr inp out
onPush :: forall (v :: T) (inp :: [T]) (out :: [T]).
(HasCallStack, ConstantScope v) =>
Value v -> Instr inp out
onPush Value v
v = case Value v -> Maybe TypicalFailWith
forall (t :: T).
ConstantScope t =>
Value t -> Maybe TypicalFailWith
isTypicalErrorConstant Value v
v of
Just (FailWithString (MText -> SomeConstant
f -> SomeConstant Value t
v')) -> Value t -> Instr inp (t : inp)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value t
v' Instr inp (t : inp) -> Instr (t : inp) out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (t : inp) out
forall (a :: T) (s :: [T]) (out :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : s) out
FAILWITH
Just (FailWithConstantPair (MText -> SomeConstant
f -> SomeConstant Value t
v') (SomeConstant Value t
arg)) ->
Value' Instr ('TPair t t) -> Instr inp ('TPair t t : inp)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH ((Value t, Value t) -> Value' Instr ('TPair t t)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value t
v', Value t
arg)) Instr inp ('TPair t t : inp)
-> Instr ('TPair t t : inp) out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr ('TPair t t : inp) out
forall (a :: T) (s :: [T]) (out :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : s) out
FAILWITH
Just TypicalFailWith
_ -> Text -> Instr inp out
forall a. HasCallStack => Text -> a
error Text
"Unexpected TypicalFailWith"
Maybe TypicalFailWith
Nothing -> Value v -> Instr inp (v : inp)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value v
v Instr inp (v : inp) -> Instr (v : inp) out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (v : inp) out
forall (a :: T) (s :: [T]) (out :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : s) out
FAILWITH