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

-- | Typical usages of FAILWITH instruction.

module Michelson.FailPattern
  ( TypicalFailWith
  , typicalFailWithTag
  , isTypicalFailWith
  , modifyTypicalFailWith

  , ConstantScope'
  ) where

import Michelson.Text (MText)
import Michelson.Typed

-- | We need this class to pass it to 'SomeConstrainedValue'.
-- 'ConstantScope' is needed because we push a value and 'Typeable' is
-- needed for 'FAILWITH'.
class (Typeable a, ConstantScope a) => ConstantScope' a
instance (Typeable a, ConstantScope a) => ConstantScope' a

-- | This data type captures typical ways to use `FAILWITH` instruction.
-- Each constructor corresponds to a usage pattern.
data TypicalFailWith
  = FailWithString MText
  -- ^ Push a constant string and fail with it.
  | FailWithConstantPair MText (SomeConstrainedValue ConstantScope')
  -- ^ Push a constant pair where the first item is a string and the
  -- second one is an arbitrary constant. Fail afterwards.
  | FailWithStackValue MText
  -- ^ Push a constant string and apply the 'PAIR' instruction, then fail.

-- | Extract error tag out of 'TypicalFailWith'.
typicalFailWithTag :: TypicalFailWith -> MText
typicalFailWithTag :: TypicalFailWith -> MText
typicalFailWithTag = \case
  FailWithString str :: MText
str -> MText
str
  FailWithConstantPair str :: MText
str _ -> MText
str
  FailWithStackValue str :: MText
str -> MText
str

-- | Check whether given instruction ends with a typical 'FAILWITH'
-- usage. It does not recursively check instructions that can be
-- passed to other instructions.
--
-- The instruction MUST be linearized to the left (see 'linearizeLeft').
isTypicalFailWith :: Instr inp out -> Maybe TypicalFailWith
isTypicalFailWith :: Instr inp out -> Maybe TypicalFailWith
isTypicalFailWith = \case
  Seq i1 :: Instr inp b
i1 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
  _ -> Maybe TypicalFailWith
forall a. Maybe a
Nothing
  where
    isTypicalPreFailWith ::
      Instr inp (a ': out) -> Maybe TypicalFailWith
    isTypicalPreFailWith :: Instr inp (a : out) -> Maybe TypicalFailWith
isTypicalPreFailWith =
      \case
        PUSH v :: 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 v :: 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 v :: 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 _ (PUSH v :: 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

        _ -> Maybe TypicalFailWith
forall a. Maybe a
Nothing

isTypicalErrorConstant ::
  forall t. ConstantScope t => Value t -> Maybe TypicalFailWith
isTypicalErrorConstant :: Value t -> Maybe TypicalFailWith
isTypicalErrorConstant v :: Value t
v
  | Just str :: 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 str :: MText
str, secondItem :: Value' Instr r
secondItem) <- Value t
v =
      -- We need to pattern match to deduce `singI` for second item of the pair.
      case SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @t of
        STPair {} -> TypicalFailWith -> Maybe TypicalFailWith
forall a. a -> Maybe a
Just (MText -> SomeConstrainedValue ConstantScope' -> TypicalFailWith
FailWithConstantPair MText
str (Value' Instr r -> SomeConstrainedValue ConstantScope'
forall (t :: T) (c :: T -> Constraint) (instr :: [T] -> [T] -> *).
c t =>
Value' instr t -> SomeConstrainedValue' instr c
SomeConstrainedValue Value' Instr r
secondItem))
  | Bool
otherwise = Maybe TypicalFailWith
forall a. Maybe a
Nothing

-- | If given instruction ends with a typical 'FAILWITH' usage, modify
-- the tag used there using given transformation function. It can
-- return any value, not necessarily a string.
modifyTypicalFailWith
  :: HasCallStack
  => (MText -> SomeConstrainedValue ConstantScope')
  -> Instr inp out
  -> Instr inp out
modifyTypicalFailWith :: (MText -> SomeConstrainedValue ConstantScope')
-> Instr inp out -> Instr inp out
modifyTypicalFailWith f :: MText -> SomeConstrainedValue ConstantScope'
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' :: Instr inp out -> Instr inp out
modifyTypicalFailWith' =
      \case
        Seq i1 :: Instr inp b
i1 FAILWITH ->
          case Instr inp b
i1 of
            PUSH v :: Value' Instr t
v -> Value' Instr t -> Instr inp out
forall (v :: T) (inp :: [T]) (out :: [T]).
(HasCallStack, Typeable v, ConstantScope v) =>
Value v -> Instr inp out
onPush Value' Instr t
v
            Seq i0 :: Instr inp b
i0 (PUSH v :: Value' Instr t
v) -> Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr inp b
i0 (Value' Instr t -> Instr b out
forall (v :: T) (inp :: [T]) (out :: [T]).
(HasCallStack, Typeable v, ConstantScope v) =>
Value v -> Instr inp out
onPush Value' Instr t
v)

            -- It is quite hard to move the body of these very similar
            -- cases into a separate function because involved types
            -- are quite sophisticated.
            Seq (PUSH v :: Value' Instr t
v) PAIR
              | Value' Instr t
_ :: Value a <- Value' Instr t
v
              , _ :: Instr (b ': s) ('TPair a b ': s) <- Instr inp b
i1 ->
                case SingI ('TPair t b) => Sing ('TPair t b)
forall k (a :: k). SingI a => Sing a
sing @('TPair a b) of
                  STPair {} -> case Value' Instr t -> Maybe MText
forall (t :: T). Value t -> Maybe MText
isStringValue Value' Instr t
v of
                    Just (MText -> SomeConstrainedValue ConstantScope'
f -> SomeConstrainedValue v' :: Value' Instr t
v') ->
                      Value' Instr t -> Instr inp (t : inp)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr t
v' Instr inp (t : inp)
-> Instr (t : inp) ('TPair t b : s) -> Instr inp ('TPair t b : s)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr (t : inp) ('TPair t b : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ (a : b : s), o ~ ('TPair a b : s)) =>
Instr i o
PAIR Instr inp ('TPair t b : s)
-> Instr ('TPair t b : s) out -> Instr inp out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr ('TPair t b : s) out
forall (a :: T) (s :: [T]) (t :: [T]). KnownT a => Instr (a : s) t
FAILWITH
                    Nothing ->
                      Value' Instr t -> Instr inp (t : inp)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr t
v Instr inp (t : inp)
-> Instr (t : inp) ('TPair t b : s) -> Instr inp ('TPair t b : s)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr (t : inp) ('TPair t b : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ (a : b : s), o ~ ('TPair a b : s)) =>
Instr i o
PAIR Instr inp ('TPair t b : s)
-> Instr ('TPair t b : s) out -> Instr inp out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr ('TPair t b : s) out
forall (a :: T) (s :: [T]) (t :: [T]). KnownT a => Instr (a : s) t
FAILWITH
            Seq (Seq i0 :: Instr inp b
i0 (PUSH v :: Value' Instr t
v)) PAIR
              | Value' Instr t
_ :: Value a <- Value' Instr t
v
              , _ :: Instr s0 ('TPair a b ': s) <- Instr inp b
i1 ->
                case SingI ('TPair t b) => Sing ('TPair t b)
forall k (a :: k). SingI a => Sing a
sing @('TPair a b) of
                  STPair {} -> Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
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 -> SomeConstrainedValue ConstantScope'
f -> SomeConstrainedValue v' :: Value' Instr t
v') ->
                      Value' Instr t -> Instr b (t : b)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr t
v' Instr b (t : b)
-> Instr (t : b) ('TPair t b : s) -> Instr b ('TPair t b : s)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr (t : b) ('TPair t b : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ (a : b : s), o ~ ('TPair a b : s)) =>
Instr i o
PAIR Instr b ('TPair t b : s)
-> Instr ('TPair t b : s) out -> Instr b out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr ('TPair t b : s) out
forall (a :: T) (s :: [T]) (t :: [T]). KnownT a => Instr (a : s) t
FAILWITH
                    Nothing ->
                      Value' Instr t -> Instr b (t : b)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr t
v Instr b (t : b)
-> Instr (t : b) ('TPair t b : s) -> Instr b ('TPair t b : s)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr (t : b) ('TPair t b : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ (a : b : s), o ~ ('TPair a b : s)) =>
Instr i o
PAIR Instr b ('TPair t b : s)
-> Instr ('TPair t b : s) out -> Instr b out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr ('TPair t b : s) out
forall (a :: T) (s :: [T]) (t :: [T]). KnownT a => Instr (a : s) t
FAILWITH

            _ -> Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr inp b
i1 Instr b out
forall (a :: T) (s :: [T]) (t :: [T]). KnownT a => Instr (a : s) t
FAILWITH

        i :: Instr inp out
i -> Instr inp out
i

    onPush ::
      (HasCallStack, Typeable v, ConstantScope v) => Value v -> Instr inp out
    onPush :: Value v -> Instr inp out
onPush v :: 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 -> SomeConstrainedValue ConstantScope'
f -> SomeConstrainedValue v' :: Value' Instr t
v')) -> Value' Instr t -> Instr inp (t : inp)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr t
v' Instr inp (t : inp) -> Instr (t : inp) out -> Instr inp out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr (t : inp) out
forall (a :: T) (s :: [T]) (t :: [T]). KnownT a => Instr (a : s) t
FAILWITH
      Just (FailWithConstantPair (MText -> SomeConstrainedValue ConstantScope'
f -> SomeConstrainedValue v' :: Value' Instr t
v') (SomeConstrainedValue arg :: Value' Instr t
arg)) ->
        Value' Instr ('TPair t t) -> Instr inp ('TPair t t : inp)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH ((Value' Instr t, Value' Instr 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' Instr t
v', Value' Instr t
arg)) Instr inp ('TPair t t : inp)
-> Instr ('TPair t t : inp) out -> Instr inp out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr ('TPair t t : inp) out
forall (a :: T) (s :: [T]) (t :: [T]). KnownT a => Instr (a : s) t
FAILWITH
      Just _ -> Text -> Instr inp out
forall a. HasCallStack => Text -> a
error "Unexpected TypicalFailWith"
      Nothing -> Value v -> Instr inp (v : inp)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value v
v Instr inp (v : inp) -> Instr (v : inp) out -> Instr inp out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr (v : inp) out
forall (a :: T) (s :: [T]) (t :: [T]). KnownT a => Instr (a : s) t
FAILWITH