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

-- | General-purpose utility functions for typed types.

module Michelson.Typed.Util
  ( DfsSettings (..)
  , CtorEffectsApp (..)
  , ceaBottomToTop
  , dfsInstr
  , dfsFoldInstr
  , dfsModifyInstr

  -- * Changing instruction tree structure
  , linearizeLeft
  , linearizeLeftDeep

  -- * Value analysis
  , dfsValue
  , dfsFoldValue
  , dfsModifyValue
  , isStringValue
  , isBytesValue
  , allAtomicValues
  ) where

import Prelude hiding (Ordering(..))

import Data.Default (Default(..))
import qualified Data.Foldable as F
import qualified Data.Map as M
import qualified Data.Set as S
import qualified Text.Show

import Michelson.Text (MText)
import Michelson.Typed.Aliases
import Michelson.Typed.Instr
import Michelson.Typed.Value

-- | Options for 'dfsInstr'.
data DfsSettings x = DfsSettings
  { DfsSettings x -> Bool
dsGoToValues :: Bool
    -- ^ Whether 'dfsInstr' function should go into values which contain other
    -- instructions: lambdas and constant contracts
    -- (which can be passed to @CREATE_CONTRACT@).
  , DfsSettings x -> CtorEffectsApp x
dsCtorEffectsApp :: CtorEffectsApp x
    -- ^ How do we handle intermediate nodes in instruction tree.
  } deriving stock (Int -> DfsSettings x -> ShowS
[DfsSettings x] -> ShowS
DfsSettings x -> String
(Int -> DfsSettings x -> ShowS)
-> (DfsSettings x -> String)
-> ([DfsSettings x] -> ShowS)
-> Show (DfsSettings x)
forall x. Int -> DfsSettings x -> ShowS
forall x. [DfsSettings x] -> ShowS
forall x. DfsSettings x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DfsSettings x] -> ShowS
$cshowList :: forall x. [DfsSettings x] -> ShowS
show :: DfsSettings x -> String
$cshow :: forall x. DfsSettings x -> String
showsPrec :: Int -> DfsSettings x -> ShowS
$cshowsPrec :: forall x. Int -> DfsSettings x -> ShowS
Show)

-- | Describes how intermediate nodes in instruction tree are accounted.
data CtorEffectsApp x = CtorEffectsApp
  { CtorEffectsApp x -> Text
ceaName :: Text
    -- ^ Name of this way.
  , CtorEffectsApp x
-> forall (i :: [T]) (o :: [T]).
   Semigroup x =>
   x -> x -> Instr i o -> (Instr i o, x)
ceaApplyEffects
      :: forall i o. Semigroup x => x -> x -> Instr i o -> (Instr i o, x)
    -- ^ This function accepts:
    -- 1. Effects gathered after applying @step@ to node's children, but
    -- before applying it to the node itself.
    -- 2. Effects gathered after applying @step@ to the given intermediate node.
    -- 3. Instruction resulting after all modifications produced by @step@.
  }

instance Show (CtorEffectsApp x) where
  show :: CtorEffectsApp x -> String
show CtorEffectsApp{..} = Text -> String
forall b a. (Show a, IsString b) => a -> b
show Text
ceaName

-- | Gather effects first for children nodes, then for their parents.
ceaBottomToTop :: CtorEffectsApp x
ceaBottomToTop :: CtorEffectsApp x
ceaBottomToTop = $WCtorEffectsApp :: forall x.
Text
-> (forall (i :: [T]) (o :: [T]).
    Semigroup x =>
    x -> x -> Instr i o -> (Instr i o, x))
-> CtorEffectsApp x
CtorEffectsApp
  { ceaName :: Text
ceaName = "Apply after"
  , ceaApplyEffects :: forall (i :: [T]) (o :: [T]).
Semigroup x =>
x -> x -> Instr i o -> (Instr i o, x)
ceaApplyEffects =
      \effBefore :: x
effBefore effAfter :: x
effAfter instr :: Instr i o
instr -> (Instr i o
instr, x
effBefore x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
effAfter)
  }

instance Default (DfsSettings x) where
  def :: DfsSettings x
def = $WDfsSettings :: forall x. Bool -> CtorEffectsApp x -> DfsSettings x
DfsSettings
    { dsGoToValues :: Bool
dsGoToValues = Bool
False
    , dsCtorEffectsApp :: CtorEffectsApp x
dsCtorEffectsApp = CtorEffectsApp x
forall x. CtorEffectsApp x
ceaBottomToTop
    }

-- | Traverse a typed instruction in depth-first order.
-- '<>' is used to concatenate intermediate results.
-- Each instructions can be changed using the supplied @step@ function.
-- It does not consider extra instructions (not present in Michelson).
dfsInstr ::
     forall x inp out. Semigroup x
  => DfsSettings x
  -> (forall i o. Instr i o -> (Instr i o, x))
  -> Instr inp out
  -> (Instr inp out, x)
dfsInstr :: DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr settings :: DfsSettings x
settings@DfsSettings{..} step :: forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step i :: Instr inp out
i =
  case Instr inp out
i of
    Seq i1 :: Instr inp b
i1 i2 :: Instr b out
i2 -> (Instr inp b -> Instr b out -> Instr inp out)
-> Instr inp b -> Instr b out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]) (i1 :: [T]) (o1 :: [T]) (i2 :: [T])
       (o2 :: [T]).
(Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> (Instr i o, x)
recursion2 Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
Seq Instr inp b
i1 Instr b out
i2
    WithLoc loc :: InstrCallStack
loc i1 :: Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (InstrCallStack -> Instr inp out -> Instr inp out
forall (a :: [T]) (b :: [T]).
InstrCallStack -> Instr a b -> Instr a b
WithLoc InstrCallStack
loc) Instr inp out
i1
    InstrWithNotes notes :: PackedNotes out
notes i1 :: Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (PackedNotes out -> Instr inp out -> Instr inp out
forall (b :: [T]) (a :: [T]).
PackedNotes b -> Instr a b -> Instr a b
InstrWithNotes PackedNotes out
notes) Instr inp out
i1
    InstrWithVarNotes varNotes :: NonEmpty VarAnn
varNotes i1 :: Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (NonEmpty VarAnn -> Instr inp out -> Instr inp out
forall (a :: [T]) (b :: [T]).
NonEmpty VarAnn -> Instr a b -> Instr a b
InstrWithVarNotes NonEmpty VarAnn
varNotes) Instr inp out
i1
    FrameInstr p :: Proxy s
p i1 :: Instr a b
i1 -> (Instr a b -> Instr inp out) -> Instr a b -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
forall (a :: [T]) (b :: [T]) (s :: [T]).
(KnownList a, KnownList b) =>
Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
FrameInstr Proxy s
p) Instr a b
i1
    Nested i1 :: Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
Nested Instr inp out
i1
    DocGroup dg :: DocGrouping
dg i1 :: Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (DocGrouping -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
DocGrouping -> Instr inp out -> Instr inp out
DocGroup DocGrouping
dg) Instr inp out
i1
    IF_NONE i1 :: Instr s out
i1 i2 :: Instr (a : s) out
i2 -> (Instr s out -> Instr (a : s) out -> Instr ('TOption a : s) out)
-> Instr s out
-> Instr (a : s) out
-> (Instr ('TOption a : s) out, x)
forall (i :: [T]) (o :: [T]) (i1 :: [T]) (o1 :: [T]) (i2 :: [T])
       (o2 :: [T]).
(Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> (Instr i o, x)
recursion2 Instr s out -> Instr (a : s) out -> Instr ('TOption a : s) out
forall (s :: [T]) (s' :: [T]) (a :: T).
Instr s s' -> Instr (a : s) s' -> Instr ('TOption a : s) s'
IF_NONE Instr s out
i1 Instr (a : s) out
i2
    IF_LEFT i1 :: Instr (a : s) out
i1 i2 :: Instr (b : s) out
i2 -> (Instr (a : s) out
 -> Instr (b : s) out -> Instr ('TOr a b : s) out)
-> Instr (a : s) out
-> Instr (b : s) out
-> (Instr ('TOr a b : s) out, x)
forall (i :: [T]) (o :: [T]) (i1 :: [T]) (o1 :: [T]) (i2 :: [T])
       (o2 :: [T]).
(Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> (Instr i o, x)
recursion2 Instr (a : s) out -> Instr (b : s) out -> Instr ('TOr a b : s) out
forall (a :: T) (s :: [T]) (s' :: [T]) (b :: T).
Instr (a : s) s' -> Instr (b : s) s' -> Instr ('TOr a b : s) s'
IF_LEFT Instr (a : s) out
i1 Instr (b : s) out
i2
    IF_CONS i1 :: Instr (a : 'TList a : s) out
i1 i2 :: Instr s out
i2 -> (Instr (a : 'TList a : s) out
 -> Instr s out -> Instr ('TList a : s) out)
-> Instr (a : 'TList a : s) out
-> Instr s out
-> (Instr ('TList a : s) out, x)
forall (i :: [T]) (o :: [T]) (i1 :: [T]) (o1 :: [T]) (i2 :: [T])
       (o2 :: [T]).
(Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> (Instr i o, x)
recursion2 Instr (a : 'TList a : s) out
-> Instr s out -> Instr ('TList a : s) out
forall (a :: T) (s :: [T]) (s' :: [T]).
Instr (a : 'TList a : s) s'
-> Instr s s' -> Instr ('TList a : s) s'
IF_CONS Instr (a : 'TList a : s) out
i1 Instr s out
i2
    IF i1 :: Instr s out
i1 i2 :: Instr s out
i2 -> (Instr s out -> Instr s out -> Instr ('TBool : s) out)
-> Instr s out -> Instr s out -> (Instr ('TBool : s) out, x)
forall (i :: [T]) (o :: [T]) (i1 :: [T]) (o1 :: [T]) (i2 :: [T])
       (o2 :: [T]).
(Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> (Instr i o, x)
recursion2 Instr s out -> Instr s out -> Instr ('TBool : s) out
forall (s :: [T]) (s' :: [T]).
Instr s s' -> Instr s s' -> Instr ('TBool : s) s'
IF Instr s out
i1 Instr s out
i2
    MAP i1 :: Instr (MapOpInp c : s) (b : s)
i1 -> (Instr (MapOpInp c : s) (b : s) -> Instr (c : s) out)
-> Instr (MapOpInp c : s) (b : s) -> (Instr (c : s) out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 Instr (MapOpInp c : s) (b : s) -> Instr (c : s) out
forall (c :: T) (b :: T) (s :: [T]).
(MapOp c, KnownT b) =>
Instr (MapOpInp c : s) (b : s) -> Instr (c : s) (MapOpRes c b : s)
MAP Instr (MapOpInp c : s) (b : s)
i1
    ITER i1 :: Instr (IterOpEl c : out) out
i1 -> (Instr (IterOpEl c : out) out -> Instr (c : out) out)
-> Instr (IterOpEl c : out) out -> (Instr (c : out) out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 Instr (IterOpEl c : out) out -> Instr (c : out) out
forall (c :: T) (s :: [T]).
IterOp c =>
Instr (IterOpEl c : s) s -> Instr (c : s) s
ITER Instr (IterOpEl c : out) out
i1
    LOOP i1 :: Instr out ('TBool : out)
i1 -> (Instr out ('TBool : out) -> Instr ('TBool : out) out)
-> Instr out ('TBool : out) -> (Instr ('TBool : out) out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 Instr out ('TBool : out) -> Instr ('TBool : out) out
forall (s :: [T]). Instr s ('TBool : s) -> Instr ('TBool : s) s
LOOP Instr out ('TBool : out)
i1
    LOOP_LEFT i1 :: Instr (a : s) ('TOr a b : s)
i1 -> (Instr (a : s) ('TOr a b : s) -> Instr ('TOr a b : s) (b : s))
-> Instr (a : s) ('TOr a b : s)
-> (Instr ('TOr a b : s) (b : s), x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 Instr (a : s) ('TOr a b : s) -> Instr ('TOr a b : s) (b : s)
forall (a :: T) (s :: [T]) (b :: T).
Instr (a : s) ('TOr a b : s) -> Instr ('TOr a b : s) (b : s)
LOOP_LEFT Instr (a : s) ('TOr a b : s)
i1
    DIP i1 :: Instr a c
i1 -> (Instr a c -> Instr (b : a) (b : c))
-> Instr a c -> (Instr (b : a) (b : c), x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 Instr a c -> Instr (b : a) (b : c)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr a c
i1
    DIPN s :: Sing n
s i1 :: Instr s s'
i1 -> (Instr s s' -> Instr inp out) -> Instr s s' -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (Sing n -> Instr s s' -> Instr inp out
forall (n :: Peano) (inp :: [T]) (out :: [T]) (s :: [T])
       (s' :: [T]).
(ConstraintDIPN n inp out s s', NFData (Sing n)) =>
Sing n -> Instr s s' -> Instr inp out
DIPN Sing n
s) Instr s s'
i1

    -- This case is more complex so we duplicate @recursion1@ a bit.
    -- We have to traverse the pushed value because a lambda can be
    -- somewhere inside of it (e. g. one item of a pair).
    PUSH v :: Value' Instr t
v -> (Instr inp out, x)
-> Maybe (Instr inp out, x) -> (Instr inp out, x)
forall a. a -> Maybe a -> a
fromMaybe (Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i) do
        Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
dsGoToValues
        let
          valueStep :: forall t . Value t -> (Value t, Maybe x)
          valueStep :: Value t -> (Value t, Maybe x)
valueStep = \case
            -- Using 'analyzeInstrFailure' here (and in case below) is cheap
            -- (O(n) in total) because we never make it run over the same code twice
            VLam lambda :: RemFail Instr '[inp] '[out]
lambda -> (Instr '[inp] '[out] -> Value' Instr ('TLambda inp out))
-> (x -> Maybe x)
-> (Instr '[inp] '[out], x)
-> (Value' Instr ('TLambda inp out), Maybe x)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (RemFail Instr '[inp] '[out] -> Value' Instr ('TLambda inp out)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(KnownT inp, KnownT out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
RemFail instr '[inp] '[out] -> Value' instr ('TLambda inp out)
VLam (RemFail Instr '[inp] '[out] -> Value' Instr ('TLambda inp out))
-> (Instr '[inp] '[out] -> RemFail Instr '[inp] '[out])
-> Instr '[inp] '[out]
-> Value' Instr ('TLambda inp out)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr '[inp] '[out] -> RemFail Instr '[inp] '[out]
forall (i :: [T]) (o :: [T]).
HasCallStack =>
Instr i o -> RemFail Instr i o
analyzeInstrFailure) x -> Maybe x
forall a. a -> Maybe a
Just ((Instr '[inp] '[out], x) -> (Value t, Maybe x))
-> (Instr '[inp] '[out], x) -> (Value t, Maybe x)
forall a b. (a -> b) -> a -> b
$
              DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr '[inp] '[out]
-> (Instr '[inp] '[out], x)
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings x
settings forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step (RemFail Instr '[inp] '[out] -> Instr '[inp] '[out]
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
RemFail instr i o -> instr i o
rfAnyInstr RemFail Instr '[inp] '[out]
lambda)
            otherV :: Value t
otherV -> (Value t
otherV, Maybe x
forall a. Maybe a
Nothing)
        -- Note that @dfsValue@ does not respect 'CtorEffectsApp',
        -- so if we encounter a value that contains more than one lambda
        -- this function may misbehave.
        -- That's very unlikely in practice.
        -- In #264 we will support this feature in @dfsValue@.
        let
          (innerV :: Value' Instr t
innerV, innerXMaybe :: Maybe x
innerXMaybe) = (forall (t' :: T). Value t' -> (Value t', Maybe x))
-> Value' Instr t -> (Value' Instr t, Maybe x)
forall (t :: T) x.
Monoid x =>
(forall (t' :: T). Value t' -> (Value t', x))
-> Value t -> (Value t, x)
dfsValue forall (t' :: T). Value t' -> (Value t', Maybe x)
valueStep Value' Instr t
v

        x
innerX <- Maybe x
innerXMaybe
        let (outerI :: Instr inp (t : inp)
outerI, outerX :: x
outerX) = Instr inp (t : inp) -> (Instr inp (t : inp), x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step (Instr inp (t : inp) -> (Instr inp (t : inp), x))
-> Instr inp (t : inp) -> (Instr inp (t : inp), x)
forall a b. (a -> b) -> a -> b
$ 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
innerV
        pure $ CtorEffectsApp x
-> x -> x -> Instr inp (t : inp) -> (Instr inp (t : inp), x)
forall x.
CtorEffectsApp x
-> forall (i :: [T]) (o :: [T]).
   Semigroup x =>
   x -> x -> Instr i o -> (Instr i o, x)
ceaApplyEffects CtorEffectsApp x
dsCtorEffectsApp x
innerX x
outerX Instr inp (t : inp)
outerI

    LAMBDA (VLam i1 :: RemFail Instr '[inp] '[out]
i1)
      | Bool
dsGoToValues ->
          (Instr '[inp] '[out] -> Instr inp ('TLambda inp out : inp))
-> Instr '[inp] '[out] -> (Instr inp ('TLambda inp out : inp), x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (Value' Instr ('TLambda inp out)
-> Instr inp ('TLambda inp out : inp)
forall (i :: T) (o :: T) (s :: [T]).
(KnownT i, KnownT o) =>
Value' Instr ('TLambda i o) -> Instr s ('TLambda i o : s)
LAMBDA (Value' Instr ('TLambda inp out)
 -> Instr inp ('TLambda inp out : inp))
-> (Instr '[inp] '[out] -> Value' Instr ('TLambda inp out))
-> Instr '[inp] '[out]
-> Instr inp ('TLambda inp out : inp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RemFail Instr '[inp] '[out] -> Value' Instr ('TLambda inp out)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(KnownT inp, KnownT out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
RemFail instr '[inp] '[out] -> Value' instr ('TLambda inp out)
VLam (RemFail Instr '[inp] '[out] -> Value' Instr ('TLambda inp out))
-> (Instr '[inp] '[out] -> RemFail Instr '[inp] '[out])
-> Instr '[inp] '[out]
-> Value' Instr ('TLambda inp out)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr '[inp] '[out] -> RemFail Instr '[inp] '[out]
forall (i :: [T]) (o :: [T]).
HasCallStack =>
Instr i o -> RemFail Instr i o
analyzeInstrFailure) (RemFail Instr '[inp] '[out] -> Instr '[inp] '[out]
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
RemFail instr i o -> instr i o
rfAnyInstr RemFail Instr '[inp] '[out]
i1)
      | Bool
otherwise -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    CREATE_CONTRACT contract :: Contract p g
contract
      | Bool
dsGoToValues ->
        let updateContractCode :: ContractCode p g
-> Instr
     ('TOption 'TKeyHash : 'TMutez : g : s)
     ('TOperation : 'TAddress : s)
updateContractCode code :: ContractCode p g
code = Contract p g
-> Instr
     ('TOption 'TKeyHash : 'TMutez : g : s)
     ('TOperation : 'TAddress : s)
forall (p :: T) (g :: T) (s :: [T]).
(ParameterScope p, StorageScope g) =>
Contract p g
-> Instr
     ('TOption 'TKeyHash : 'TMutez : g : s)
     ('TOperation : 'TAddress : s)
CREATE_CONTRACT (Contract p g
 -> Instr
      ('TOption 'TKeyHash : 'TMutez : g : s)
      ('TOperation : 'TAddress : s))
-> Contract p g
-> Instr
     ('TOption 'TKeyHash : 'TMutez : g : s)
     ('TOperation : 'TAddress : s)
forall a b. (a -> b) -> a -> b
$ Contract p g
contract{ cCode :: ContractCode p g
cCode = ContractCode p g
code }
        in (ContractCode p g
 -> Instr
      ('TOption 'TKeyHash : 'TMutez : g : s)
      ('TOperation : 'TAddress : s))
-> ContractCode p g
-> (Instr
      ('TOption 'TKeyHash : 'TMutez : g : s)
      ('TOperation : 'TAddress : s),
    x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 ContractCode p g
-> Instr
     ('TOption 'TKeyHash : 'TMutez : g : s)
     ('TOperation : 'TAddress : s)
updateContractCode (ContractCode p g -> (Instr inp out, x))
-> ContractCode p g -> (Instr inp out, x)
forall a b. (a -> b) -> a -> b
$ Contract p g -> ContractCode p g
forall (cp :: T) (st :: T). Contract cp st -> ContractCode cp st
cCode Contract p g
contract
      | Bool
otherwise -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i

    Nop{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    Ext (TEST_ASSERT (TestAssert nm :: Text
nm pc :: PrintComment inp
pc i1 :: Instr inp ('TBool : out)
i1)) ->
      (Instr inp ('TBool : out) -> Instr inp inp)
-> Instr inp ('TBool : out) -> (Instr inp inp, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (ExtInstr inp -> Instr inp inp
forall (s :: [T]). ExtInstr s -> Instr s s
Ext (ExtInstr inp -> Instr inp inp)
-> (Instr inp ('TBool : out) -> ExtInstr inp)
-> Instr inp ('TBool : out)
-> Instr inp inp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestAssert inp -> ExtInstr inp
forall (s :: [T]). TestAssert s -> ExtInstr s
TEST_ASSERT (TestAssert inp -> ExtInstr inp)
-> (Instr inp ('TBool : out) -> TestAssert inp)
-> Instr inp ('TBool : out)
-> ExtInstr inp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text
-> PrintComment inp -> Instr inp ('TBool : out) -> TestAssert inp
forall (out :: [T]) (inp :: [T]).
Typeable out =>
Text
-> PrintComment inp -> Instr inp ('TBool : out) -> TestAssert inp
TestAssert Text
nm PrintComment inp
pc) Instr inp ('TBool : out)
i1
    Ext{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    AnnCAR{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    AnnCDR{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    DROP{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    DROPN{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    DUP{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    SWAP{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    DIG{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    DUG{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    SOME{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    NONE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    UNIT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    AnnPAIR{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    LEFT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    RIGHT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    NIL{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    CONS{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    SIZE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    EMPTY_SET{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    EMPTY_MAP{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    EMPTY_BIG_MAP{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    MEM{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    GET{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    UPDATE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    EXEC{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    APPLY{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    FAILWITH{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    CAST{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    RENAME{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    PACK{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    UNPACK{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    CONCAT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    CONCAT'{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    SLICE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    ISNAT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    ADD{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    SUB{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    MUL{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    EDIV{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    ABS{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    NEG{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    LSL{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    LSR{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    OR{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    AND{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    XOR{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    NOT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    COMPARE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    EQ{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    NEQ{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    LT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    GT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    LE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    GE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    INT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    SELF{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    CONTRACT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    TRANSFER_TOKENS{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    SET_DELEGATE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    IMPLICIT_ACCOUNT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    NOW{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    AMOUNT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    BALANCE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    CHECK_SIGNATURE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    SHA256{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    SHA512{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    BLAKE2B{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    SHA3{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    KECCAK{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    HASH_KEY{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    SOURCE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    SENDER{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    ADDRESS{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    CHAIN_ID{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
    LEVEL{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
  where
    recursion1 ::
      forall a b c d. (Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
    recursion1 :: (Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 constructor :: Instr a b -> Instr c d
constructor i0 :: Instr a b
i0 =
      let
        (innerI :: Instr a b
innerI, innerX :: x
innerX) = DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr a b
-> (Instr a b, x)
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings x
settings forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr a b
i0
        (outerI :: Instr c d
outerI, outerX :: x
outerX) = Instr c d -> (Instr c d, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step (Instr c d -> (Instr c d, x)) -> Instr c d -> (Instr c d, x)
forall a b. (a -> b) -> a -> b
$ Instr a b -> Instr c d
constructor Instr a b
innerI
      in CtorEffectsApp x -> x -> x -> Instr c d -> (Instr c d, x)
forall x.
CtorEffectsApp x
-> forall (i :: [T]) (o :: [T]).
   Semigroup x =>
   x -> x -> Instr i o -> (Instr i o, x)
ceaApplyEffects CtorEffectsApp x
dsCtorEffectsApp x
innerX x
outerX Instr c d
outerI

    recursion2 ::
      forall i o i1 o1 i2 o2.
      (Instr i1 o1 -> Instr i2 o2 -> Instr i o) ->
      Instr i1 o1 -> Instr i2 o2 -> (Instr i o, x)
    recursion2 :: (Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> (Instr i o, x)
recursion2 constructor :: Instr i1 o1 -> Instr i2 o2 -> Instr i o
constructor i1 :: Instr i1 o1
i1 i2 :: Instr i2 o2
i2 =
      let
        (i1' :: Instr i1 o1
i1', x1 :: x
x1) = DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr i1 o1
-> (Instr i1 o1, x)
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings x
settings forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr i1 o1
i1
        (i2' :: Instr i2 o2
i2', x2 :: x
x2) = DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr i2 o2
-> (Instr i2 o2, x)
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings x
settings forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr i2 o2
i2
        (i' :: Instr i o
i', x :: x
x) = Instr i o -> (Instr i o, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step (Instr i o -> (Instr i o, x)) -> Instr i o -> (Instr i o, x)
forall a b. (a -> b) -> a -> b
$ Instr i1 o1 -> Instr i2 o2 -> Instr i o
constructor Instr i1 o1
i1' Instr i2 o2
i2'
      in CtorEffectsApp x -> x -> x -> Instr i o -> (Instr i o, x)
forall x.
CtorEffectsApp x
-> forall (i :: [T]) (o :: [T]).
   Semigroup x =>
   x -> x -> Instr i o -> (Instr i o, x)
ceaApplyEffects CtorEffectsApp x
dsCtorEffectsApp (x
x1 x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
x2) x
x Instr i o
i'

-- | Specialization of 'dfsInstr' for case when changing the instruction is
-- not required.
dfsFoldInstr
  :: forall x inp out.
      (Semigroup x)
  => DfsSettings x
  -> (forall i o. Instr i o -> x)
  -> Instr inp out
  -> x
dfsFoldInstr :: DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> x)
-> Instr inp out
-> x
dfsFoldInstr settings :: DfsSettings x
settings step :: forall (i :: [T]) (o :: [T]). Instr i o -> x
step instr :: Instr inp out
instr =
  (Instr inp out, x) -> x
forall a b. (a, b) -> b
snd ((Instr inp out, x) -> x) -> (Instr inp out, x) -> x
forall a b. (a -> b) -> a -> b
$ DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings x
settings (\i :: Instr i o
i -> (Instr i o
i, Instr i o -> x
forall (i :: [T]) (o :: [T]). Instr i o -> x
step Instr i o
i)) Instr inp out
instr

-- | Specialization of 'dfsInstr' which only modifies given instruction.
dfsModifyInstr
  :: DfsSettings ()
  -> (forall i o. Instr i o -> Instr i o)
  -> Instr inp out
  -> Instr inp out
dfsModifyInstr :: DfsSettings ()
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
dfsModifyInstr settings :: DfsSettings ()
settings step :: forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
step instr :: Instr inp out
instr =
  (Instr inp out, ()) -> Instr inp out
forall a b. (a, b) -> a
fst ((Instr inp out, ()) -> Instr inp out)
-> (Instr inp out, ()) -> Instr inp out
forall a b. (a -> b) -> a -> b
$ DfsSettings ()
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, ()))
-> Instr inp out
-> (Instr inp out, ())
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings ()
settings (\i :: Instr i o
i -> (Instr i o -> Instr i o
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
step Instr i o
i, ())) Instr inp out
instr

-- | Check whether instruction fails at each execution path or have at least one
-- non-failing path.
--
-- This function assumes that given instruction contains no dead code
-- (contract with dead code cannot be valid Michelson contract) and may behave
-- in unexpected way if such is present. Term "dead code" includes instructions
-- which render into empty Michelson, like Morley extensions.
-- On the other hand, this function does not traverse the whole instruction tree;
-- performs fastest on left-growing combs.
--
-- Often we already have information about instruction failure, use this
-- function only in cases when this info is actually unavailable or hard
-- to use.
analyzeInstrFailure :: HasCallStack => Instr i o -> RemFail Instr i o
analyzeInstrFailure :: Instr i o -> RemFail Instr i o
analyzeInstrFailure = Instr i o -> RemFail Instr i o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go
  where
  go :: Instr i o -> RemFail Instr i o
  go :: Instr i o -> RemFail Instr i o
go = \case
    WithLoc loc :: InstrCallStack
loc i :: Instr i o
i -> case Instr i o -> RemFail Instr i o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr i o
i of
      RfNormal i0 :: Instr i o
i0 ->
        Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (InstrCallStack -> Instr i o -> Instr i o
forall (a :: [T]) (b :: [T]).
InstrCallStack -> Instr a b -> Instr a b
WithLoc InstrCallStack
loc Instr i o
i0)
      r :: RemFail Instr i o
r -> RemFail Instr i o
r
    InstrWithNotes pn :: PackedNotes o
pn i :: Instr i o
i -> case Instr i o -> RemFail Instr i o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr i o
i of
      RfNormal i0 :: Instr i o
i0 ->
        Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (PackedNotes o -> Instr i o -> Instr i o
forall (b :: [T]) (a :: [T]).
PackedNotes b -> Instr a b -> Instr a b
InstrWithNotes PackedNotes o
pn Instr i o
i0)
      RfAlwaysFails i0 :: forall (o' :: [T]). Instr i o'
i0 ->
        Text -> RemFail Instr i o
forall a. HasCallStack => Text -> a
error (Text -> RemFail Instr i o) -> Text -> RemFail Instr i o
forall a b. (a -> b) -> a -> b
$ "InstrWithNotes wraps always-failing instruction: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Instr i Any -> Text
forall b a. (Show a, IsString b) => a -> b
show Instr i Any
forall (o' :: [T]). Instr i o'
i0
    InstrWithVarNotes vn :: NonEmpty VarAnn
vn i :: Instr i o
i -> case Instr i o -> RemFail Instr i o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr i o
i of
      RfNormal i0 :: Instr i o
i0 ->
        Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (NonEmpty VarAnn -> Instr i o -> Instr i o
forall (a :: [T]) (b :: [T]).
NonEmpty VarAnn -> Instr a b -> Instr a b
InstrWithVarNotes NonEmpty VarAnn
vn Instr i o
i0)
      RfAlwaysFails i0 :: forall (o' :: [T]). Instr i o'
i0 ->
        Text -> RemFail Instr i o
forall a. HasCallStack => Text -> a
error (Text -> RemFail Instr i o) -> Text -> RemFail Instr i o
forall a b. (a -> b) -> a -> b
$ "InstrWithVarNotes wraps always-failing instruction: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Instr i Any -> Text
forall b a. (Show a, IsString b) => a -> b
show Instr i Any
forall (o' :: [T]). Instr i o'
i0
    FrameInstr s :: Proxy s
s i :: Instr a b
i -> case Instr a b -> RemFail Instr a b
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr a b
i of
      RfNormal i0 :: Instr a b
i0 ->
        Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
forall (a :: [T]) (b :: [T]) (s :: [T]).
(KnownList a, KnownList b) =>
Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
FrameInstr Proxy s
s Instr a b
i0)
      RfAlwaysFails i0 :: forall (o' :: [T]). Instr a o'
i0 ->
        Text -> RemFail Instr i o
forall a. HasCallStack => Text -> a
error (Text -> RemFail Instr i o) -> Text -> RemFail Instr i o
forall a b. (a -> b) -> a -> b
$ "FrameInstr wraps always-failing instruction: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Instr a Any -> Text
forall b a. (Show a, IsString b) => a -> b
show Instr a Any
forall (o' :: [T]). Instr a o'
i0
    Seq a :: Instr i b
a b :: Instr b o
b -> Instr i b -> Instr b o' -> Instr i o'
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
Seq Instr i b
a (forall (o' :: [T]). Instr b o' -> Instr i o')
-> RemFail Instr b o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i1 :: k) (i2 :: k) (o :: k).
(forall (o' :: k). instr i1 o' -> instr i2 o')
-> RemFail instr i1 o -> RemFail instr i2 o
`rfMapAnyInstr` Instr b o -> RemFail Instr b o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr b o
b
    Nop -> Instr i i -> RemFail Instr i i
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i i
forall (s :: [T]). Instr s s
Nop
    Ext e :: ExtInstr i
e -> Instr i i -> RemFail Instr i i
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (ExtInstr i -> Instr i i
forall (s :: [T]). ExtInstr s -> Instr s s
Ext ExtInstr i
e)
    Nested i :: Instr i o
i -> forall (o' :: [T]). Instr i o' -> Instr i o'
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
Nested (forall (o' :: [T]). Instr i o' -> Instr i o')
-> RemFail Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i1 :: k) (i2 :: k) (o :: k).
(forall (o' :: k). instr i1 o' -> instr i2 o')
-> RemFail instr i1 o -> RemFail instr i2 o
`rfMapAnyInstr` Instr i o -> RemFail Instr i o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr i o
i
    DocGroup g :: DocGrouping
g i :: Instr i o
i -> DocGrouping -> Instr i o' -> Instr i o'
forall (inp :: [T]) (out :: [T]).
DocGrouping -> Instr inp out -> Instr inp out
DocGroup DocGrouping
g (forall (o' :: [T]). Instr i o' -> Instr i o')
-> RemFail Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i1 :: k) (i2 :: k) (o :: k).
(forall (o' :: k). instr i1 o' -> instr i2 o')
-> RemFail instr i1 o -> RemFail instr i2 o
`rfMapAnyInstr` Instr i o -> RemFail Instr i o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr i o
i

    IF_NONE l :: Instr s o
l r :: Instr (a : s) o
r -> (forall (o' :: [T]). Instr s o' -> Instr (a : s) o' -> Instr i o')
-> RemFail Instr s o
-> RemFail Instr (a : s) o
-> RemFail Instr i o
forall k (instr :: k -> k -> *) (i1 :: k) (i2 :: k) (i3 :: k)
       (o :: k).
(forall (o' :: k). instr i1 o' -> instr i2 o' -> instr i3 o')
-> RemFail instr i1 o -> RemFail instr i2 o -> RemFail instr i3 o
rfMerge forall (o' :: [T]). Instr s o' -> Instr (a : s) o' -> Instr i o'
forall (s :: [T]) (s' :: [T]) (a :: T).
Instr s s' -> Instr (a : s) s' -> Instr ('TOption a : s) s'
IF_NONE (Instr s o -> RemFail Instr s o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr s o
l) (Instr (a : s) o -> RemFail Instr (a : s) o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr (a : s) o
r)
    IF_LEFT l :: Instr (a : s) o
l r :: Instr (b : s) o
r -> (forall (o' :: [T]).
 Instr (a : s) o' -> Instr (b : s) o' -> Instr i o')
-> RemFail Instr (a : s) o
-> RemFail Instr (b : s) o
-> RemFail Instr i o
forall k (instr :: k -> k -> *) (i1 :: k) (i2 :: k) (i3 :: k)
       (o :: k).
(forall (o' :: k). instr i1 o' -> instr i2 o' -> instr i3 o')
-> RemFail instr i1 o -> RemFail instr i2 o -> RemFail instr i3 o
rfMerge forall (o' :: [T]).
Instr (a : s) o' -> Instr (b : s) o' -> Instr i o'
forall (a :: T) (s :: [T]) (s' :: [T]) (b :: T).
Instr (a : s) s' -> Instr (b : s) s' -> Instr ('TOr a b : s) s'
IF_LEFT (Instr (a : s) o -> RemFail Instr (a : s) o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr (a : s) o
l) (Instr (b : s) o -> RemFail Instr (b : s) o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr (b : s) o
r)
    IF_CONS l :: Instr (a : 'TList a : s) o
l r :: Instr s o
r -> (forall (o' :: [T]).
 Instr (a : 'TList a : s) o' -> Instr s o' -> Instr i o')
-> RemFail Instr (a : 'TList a : s) o
-> RemFail Instr s o
-> RemFail Instr i o
forall k (instr :: k -> k -> *) (i1 :: k) (i2 :: k) (i3 :: k)
       (o :: k).
(forall (o' :: k). instr i1 o' -> instr i2 o' -> instr i3 o')
-> RemFail instr i1 o -> RemFail instr i2 o -> RemFail instr i3 o
rfMerge forall (o' :: [T]).
Instr (a : 'TList a : s) o' -> Instr s o' -> Instr i o'
forall (a :: T) (s :: [T]) (s' :: [T]).
Instr (a : 'TList a : s) s'
-> Instr s s' -> Instr ('TList a : s) s'
IF_CONS (Instr (a : 'TList a : s) o -> RemFail Instr (a : 'TList a : s) o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr (a : 'TList a : s) o
l) (Instr s o -> RemFail Instr s o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr s o
r)
    IF l :: Instr s o
l r :: Instr s o
r -> (forall (o' :: [T]). Instr s o' -> Instr s o' -> Instr i o')
-> RemFail Instr s o -> RemFail Instr s o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i1 :: k) (i2 :: k) (i3 :: k)
       (o :: k).
(forall (o' :: k). instr i1 o' -> instr i2 o' -> instr i3 o')
-> RemFail instr i1 o -> RemFail instr i2 o -> RemFail instr i3 o
rfMerge forall (o' :: [T]). Instr s o' -> Instr s o' -> Instr i o'
forall (s :: [T]) (s' :: [T]).
Instr s s' -> Instr s s' -> Instr ('TBool : s) s'
IF (Instr s o -> RemFail Instr s o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr s o
l) (Instr s o -> RemFail Instr s o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr s o
r)

    i :: Instr i o
i@MAP{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@ITER{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@LOOP{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@LOOP_LEFT{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@LAMBDA{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@DIP{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@DIPN{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i

    i :: Instr i o
i@AnnCAR{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@AnnCDR{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@DROP{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@DROPN{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@DUP{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@SWAP{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@DIG{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@DUG{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@PUSH{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@SOME{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@NONE{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@UNIT{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@AnnPAIR{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@LEFT{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@RIGHT{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@NIL{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@CONS{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@SIZE{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@EMPTY_SET{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@EMPTY_MAP{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@EMPTY_BIG_MAP{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@MEM{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@GET{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@UPDATE{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@EXEC{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@APPLY{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    FAILWITH -> (forall (o' :: [T]). Instr i o') -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
(forall (o' :: k). instr i o') -> RemFail instr i o
RfAlwaysFails forall (o' :: [T]). Instr i o'
forall (a :: T) (s :: [T]) (t :: [T]). KnownT a => Instr (a : s) t
FAILWITH
    i :: Instr i o
i@Instr i o
CAST -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
RENAME -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
PACK -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
UNPACK -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
CONCAT -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
CONCAT' -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
SLICE -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
ISNAT -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
ADD -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
SUB -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
MUL -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
EDIV -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
ABS -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
NEG -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
LSL -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
LSR -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
OR -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
AND -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
XOR -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
NOT -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
COMPARE -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
EQ -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
NEQ -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
LT -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
GT -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
LE -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
GE -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
INT -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@SELF{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@CONTRACT{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
TRANSFER_TOKENS -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
SET_DELEGATE -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@CREATE_CONTRACT{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
IMPLICIT_ACCOUNT -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
NOW -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
AMOUNT -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
BALANCE -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
CHECK_SIGNATURE -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
SHA256 -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
SHA512 -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
BLAKE2B -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
SHA3 -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
KECCAK -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
HASH_KEY -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
SOURCE -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
SENDER -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
ADDRESS -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
CHAIN_ID -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
    i :: Instr i o
i@Instr i o
LEVEL -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i

-- | There are many ways to represent a sequence of more than 2 instructions.
-- E. g. for @i1; i2; i3@ it can be @Seq i1 $ Seq i2 i3@ or @Seq (Seq i1 i2) i3@.
-- This function enforces a particular structure. Specifically, it makes each
-- 'Seq' have a single instruction (i. e. not 'Seq') in its second argument.
-- This function also erases redundant 'Nop's.
--
-- Please note that this function is not recursive, it does not
-- linearize contents of @IF@ and similar instructions.
linearizeLeft :: Instr inp out -> Instr inp out
linearizeLeft :: Instr inp out -> Instr inp out
linearizeLeft = Bool -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
Bool -> Instr inp out -> Instr inp out
linearizeLeftHelper Bool
False
  where
    -- In order to avoid quadratic performance we make a simple optimization.
    -- We track whether left argument of `Seq` is already linearized.
    -- If it is, we do not need to ever linearize it again.
    linearizeLeftHelper :: Bool -> Instr inp out -> Instr inp out
    linearizeLeftHelper :: Bool -> Instr inp out -> Instr inp out
linearizeLeftHelper isLeftInstrAlreadyLinear :: Bool
isLeftInstrAlreadyLinear =
      \case
        Seq i1 :: Instr inp b
i1 (Seq i2 :: Instr b b
i2 i3 :: Instr b out
i3) ->
          Bool -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
Bool -> Instr inp out -> Instr inp out
linearizeLeftHelper Bool
True (Instr inp out -> Instr inp out) -> Instr inp out -> Instr inp out
forall a b. (a -> b) -> a -> b
$
          Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
Seq (Bool -> Instr inp b -> Instr inp b
forall (inp :: [T]) (out :: [T]).
Bool -> Instr inp out -> Instr inp out
linearizeLeftHelper Bool
isLeftInstrAlreadyLinear (Instr inp b -> Instr b b -> Instr inp b
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
Seq Instr inp b
i1 Instr b b
i2)) Instr b out
i3
        -- `i2` is not a `Seq`, so we only need to linearize `i1`
        -- and connect it with `i2`.
        Seq i1 :: Instr inp b
i1 i2 :: Instr b out
i2
          | Bool
isLeftInstrAlreadyLinear
          , Instr b out
Nop <- Instr b out
i2 -> Instr inp out
Instr inp b
i1
          | Bool
isLeftInstrAlreadyLinear -> Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
Seq Instr inp b
i1 Instr b out
i2
          | Instr b out
Nop <- Instr b out
i2 -> Instr inp b -> Instr inp b
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
linearizeLeft Instr inp b
i1
          | Bool
otherwise -> Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
Seq (Instr inp b -> Instr inp b
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
linearizeLeft Instr inp b
i1) Instr b out
i2
        i :: Instr inp out
i -> Instr inp out
i

-- | "Deep" version of 'linearizeLeft'. It recursively linearizes
-- instructions stored in other instructions.
linearizeLeftDeep :: Instr inp out -> Instr inp out
linearizeLeftDeep :: Instr inp out -> Instr inp out
linearizeLeftDeep = DfsSettings ()
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
forall (inp :: [T]) (out :: [T]).
DfsSettings ()
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
dfsModifyInstr DfsSettings ()
forall a. Default a => a
def forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
linearizeLeft

----------------------------------------------------------------------------
-- Value analysis
----------------------------------------------------------------------------

-- | Traverse a value in depth-first order.
dfsValue ::
     forall t x.
     Monoid x
  => (forall t'. Value t' -> (Value t', x))
  -> Value t
  -> (Value t, x)
dfsValue :: (forall (t' :: T). Value t' -> (Value t', x))
-> Value t -> (Value t, x)
dfsValue step :: forall (t' :: T). Value t' -> (Value t', x)
step i :: Value t
i = case Value t
i of
  -- Atomic
  VKey{} -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i
  VUnit -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i
  VSignature{} -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i
  VChainId{} -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i
  VOp{} -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i
  VContract{} -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i
  VLam{} -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i
  VInt{} -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i
  VNat{} -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i
  VString{} -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i
  VBytes{} -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i
  VMutez{} -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i
  VBool{} -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i
  VKeyHash{} -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i
  VTimestamp{} -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i
  VAddress{} -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i

  -- Non-atomic
  VOption mVal :: Maybe (Value' Instr t)
mVal -> case Maybe (Value' Instr t)
mVal of
    Nothing -> Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value t
i
    Just val :: Value' Instr t
val -> (Value' Instr t -> Value t) -> Value' Instr t -> (Value t, x)
forall (t' :: T). (Value t' -> Value t) -> Value t' -> (Value t, x)
recursion1 (Maybe (Value' Instr t) -> Value' Instr ('TOption t)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value' Instr t) -> Value' Instr ('TOption t))
-> (Value' Instr t -> Maybe (Value' Instr t))
-> Value' Instr t
-> Value' Instr ('TOption t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' Instr t -> Maybe (Value' Instr t)
forall a. a -> Maybe a
Just) Value' Instr t
val
  VList vals :: [Value' Instr t]
vals ->
    let
      (vs :: [Value' Instr t]
vs, xs :: [x]
xs) = [(Value' Instr t, x)] -> ([Value' Instr t], [x])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Value' Instr t, x)] -> ([Value' Instr t], [x]))
-> [(Value' Instr t, x)] -> ([Value' Instr t], [x])
forall a b. (a -> b) -> a -> b
$ (Value' Instr t -> (Value' Instr t, x))
-> [Value' Instr t] -> [(Value' Instr t, x)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map ((forall (t' :: T). Value t' -> (Value t', x))
-> Value' Instr t -> (Value' Instr t, x)
forall (t :: T) x.
Monoid x =>
(forall (t' :: T). Value t' -> (Value t', x))
-> Value t -> (Value t, x)
dfsValue forall (t' :: T). Value t' -> (Value t', x)
step) [Value' Instr t]
vals
      (v :: Value ('TList t)
v, x :: x
x) = Value ('TList t) -> (Value ('TList t), x)
forall (t' :: T). Value t' -> (Value t', x)
step (Value ('TList t) -> (Value ('TList t), x))
-> Value ('TList t) -> (Value ('TList t), x)
forall a b. (a -> b) -> a -> b
$ [Value' Instr t] -> Value ('TList t)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
[Value' instr t] -> Value' instr ('TList t)
VList [Value' Instr t]
vs
    in
      (Value t
Value ('TList t)
v, x
x x -> x -> x
forall a. Semigroup a => a -> a -> a
<> [x] -> x
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
F.fold [x]
xs)
  VSet vals :: Set (Value' Instr t)
vals ->
    let
      (cs :: Set (Value' Instr t)
cs, cxs :: x
cxs) =
        (Value' Instr t
 -> (Set (Value' Instr t), x) -> (Set (Value' Instr t), x))
-> (Set (Value' Instr t), x)
-> Set (Value' Instr t)
-> (Set (Value' Instr t), x)
forall a b. (a -> b -> b) -> b -> Set a -> b
S.foldr (\a :: Value' Instr t
a (s :: Set (Value' Instr t)
s, xs :: x
xs) -> let (c :: Value' Instr t
c, x :: x
x) = Value' Instr t -> (Value' Instr t, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value' Instr t
a in (Value' Instr t -> Set (Value' Instr t) -> Set (Value' Instr t)
forall a. Ord a => a -> Set a -> Set a
S.insert Value' Instr t
c Set (Value' Instr t)
s, x
x x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
xs))
        (Set (Value' Instr t)
forall a. Set a
S.empty, x
forall a. Monoid a => a
mempty) Set (Value' Instr t)
vals
      (v :: Value ('TSet t)
v, vx :: x
vx) = Value ('TSet t) -> (Value ('TSet t), x)
forall (t' :: T). Value t' -> (Value t', x)
step (Set (Value' Instr t) -> Value ('TSet t)
forall (t :: T) (instr :: [T] -> [T] -> *).
(KnownT t, Comparable t) =>
Set (Value' instr t) -> Value' instr ('TSet t)
VSet Set (Value' Instr t)
cs)
    in (Value t
Value ('TSet t)
v, x
vx x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
cxs)
  VPair (v1 :: Value' Instr l
v1, v2 :: Value' Instr r
v2) -> (Value' Instr l -> Value' Instr r -> Value t)
-> Value' Instr l -> Value' Instr r -> (Value t, x)
forall (t1 :: T) (t2 :: T).
(Value t1 -> Value t2 -> Value t)
-> Value t1 -> Value t2 -> (Value t, x)
recursion2 (((Value' Instr l, Value' Instr r) -> Value' Instr ('TPair l r))
-> Value' Instr l -> Value' Instr r -> Value' Instr ('TPair l r)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Value' Instr l, Value' Instr r) -> Value' Instr ('TPair l r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair) Value' Instr l
v1 Value' Instr r
v2
  VOr vEither :: Either (Value' Instr l) (Value' Instr r)
vEither -> case Either (Value' Instr l) (Value' Instr r)
vEither of
    Left v :: Value' Instr l
v -> (Value' Instr l -> Value t) -> Value' Instr l -> (Value t, x)
forall (t' :: T). (Value t' -> Value t) -> Value t' -> (Value t, x)
recursion1 (Either (Value' Instr l) (Value' Instr r) -> Value' Instr ('TOr l r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(KnownT l, KnownT r) =>
Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VOr (Either (Value' Instr l) (Value' Instr r)
 -> Value' Instr ('TOr l r))
-> (Value' Instr l -> Either (Value' Instr l) (Value' Instr r))
-> Value' Instr l
-> Value' Instr ('TOr l r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' Instr l -> Either (Value' Instr l) (Value' Instr r)
forall a b. a -> Either a b
Left) Value' Instr l
v
    Right v :: Value' Instr r
v -> (Value' Instr r -> Value t) -> Value' Instr r -> (Value t, x)
forall (t' :: T). (Value t' -> Value t) -> Value t' -> (Value t, x)
recursion1 (Either (Value' Instr l) (Value' Instr r) -> Value' Instr ('TOr l r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(KnownT l, KnownT r) =>
Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VOr (Either (Value' Instr l) (Value' Instr r)
 -> Value' Instr ('TOr l r))
-> (Value' Instr r -> Either (Value' Instr l) (Value' Instr r))
-> Value' Instr r
-> Value' Instr ('TOr l r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' Instr r -> Either (Value' Instr l) (Value' Instr r)
forall a b. b -> Either a b
Right) Value' Instr r
v
  VMap vmap :: Map (Value' Instr k) (Value' Instr v)
vmap -> (Map (Value' Instr k) (Value' Instr v) -> Value t)
-> Map (Value' Instr k) (Value' Instr v) -> (Value t, x)
forall (t' :: T) (k :: T).
Comparable k =>
(Map (Value k) (Value t') -> Value t)
-> Map (Value k) (Value t') -> (Value t, x)
mapRecursion Map (Value' Instr k) (Value' Instr v) -> Value t
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(KnownT k, KnownT v, Comparable k) =>
Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
VMap Map (Value' Instr k) (Value' Instr v)
vmap
  VBigMap vmap :: Map (Value' Instr k) (Value' Instr v)
vmap -> (Map (Value' Instr k) (Value' Instr v) -> Value t)
-> Map (Value' Instr k) (Value' Instr v) -> (Value t, x)
forall (t' :: T) (k :: T).
Comparable k =>
(Map (Value k) (Value t') -> Value t)
-> Map (Value k) (Value t') -> (Value t, x)
mapRecursion Map (Value' Instr k) (Value' Instr v) -> Value t
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(KnownT k, KnownT v, Comparable k) =>
Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
VBigMap Map (Value' Instr k) (Value' Instr v)
vmap
  where
    recursion1 ::
         forall t'.
         (Value t' -> Value t)
      -> Value t'
      -> (Value t, x)
    recursion1 :: (Value t' -> Value t) -> Value t' -> (Value t, x)
recursion1 constructor :: Value t' -> Value t
constructor i' :: Value t'
i' =
      let
        (v :: Value t'
v, x :: x
x) = (forall (t' :: T). Value t' -> (Value t', x))
-> Value t' -> (Value t', x)
forall (t :: T) x.
Monoid x =>
(forall (t' :: T). Value t' -> (Value t', x))
-> Value t -> (Value t, x)
dfsValue forall (t' :: T). Value t' -> (Value t', x)
step Value t'
i'
        (v' :: Value t
v', x' :: x
x') = Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step (Value t -> (Value t, x)) -> Value t -> (Value t, x)
forall a b. (a -> b) -> a -> b
$ Value t' -> Value t
constructor Value t'
v
      in
        (Value t
v', x
x x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
x')
    recursion2 ::
         forall t1 t2.
         (Value t1 -> Value t2 -> Value t)
      -> Value t1
      -> Value t2
      -> (Value t, x)
    recursion2 :: (Value t1 -> Value t2 -> Value t)
-> Value t1 -> Value t2 -> (Value t, x)
recursion2 constructor :: Value t1 -> Value t2 -> Value t
constructor i1 :: Value t1
i1 i2 :: Value t2
i2 =
      let
        (v1 :: Value t1
v1, x1 :: x
x1) = (forall (t' :: T). Value t' -> (Value t', x))
-> Value t1 -> (Value t1, x)
forall (t :: T) x.
Monoid x =>
(forall (t' :: T). Value t' -> (Value t', x))
-> Value t -> (Value t, x)
dfsValue forall (t' :: T). Value t' -> (Value t', x)
step Value t1
i1
        (v2 :: Value t2
v2, x2 :: x
x2) = (forall (t' :: T). Value t' -> (Value t', x))
-> Value t2 -> (Value t2, x)
forall (t :: T) x.
Monoid x =>
(forall (t' :: T). Value t' -> (Value t', x))
-> Value t -> (Value t, x)
dfsValue forall (t' :: T). Value t' -> (Value t', x)
step Value t2
i2
        (v :: Value t
v, x :: x
x) = Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step (Value t -> (Value t, x)) -> Value t -> (Value t, x)
forall a b. (a -> b) -> a -> b
$ Value t1 -> Value t2 -> Value t
constructor Value t1
v1 Value t2
v2
      in
        (Value t
v, x
x1 x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
x2 x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
x)

    mapRecursion
      :: forall t' k. Comparable k
      => (M.Map (Value k) (Value t') -> Value t)
      -> M.Map (Value k) (Value t')
      -> (Value t, x)
    mapRecursion :: (Map (Value k) (Value t') -> Value t)
-> Map (Value k) (Value t') -> (Value t, x)
mapRecursion constructor :: Map (Value k) (Value t') -> Value t
constructor vmap :: Map (Value k) (Value t')
vmap =
      let
        (ms :: Map (Value k) (Value t')
ms, cxs :: x
cxs) = (Value k
 -> Value t'
 -> (Map (Value k) (Value t'), x)
 -> (Map (Value k) (Value t'), x))
-> (Map (Value k) (Value t'), x)
-> Map (Value k) (Value t')
-> (Map (Value k) (Value t'), x)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey (\k :: Value k
k a :: Value t'
a (m :: Map (Value k) (Value t')
m, xs :: x
xs) ->
            let (c :: Value k
c, cx :: x
cx) = Value k -> (Value k, x)
forall (t' :: T). Value t' -> (Value t', x)
step Value k
k
                (v :: Value t'
v, vx :: x
vx) = (forall (t' :: T). Value t' -> (Value t', x))
-> Value t' -> (Value t', x)
forall (t :: T) x.
Monoid x =>
(forall (t' :: T). Value t' -> (Value t', x))
-> Value t -> (Value t, x)
dfsValue forall (t' :: T). Value t' -> (Value t', x)
step Value t'
a
            in (Value k
-> Value t' -> Map (Value k) (Value t') -> Map (Value k) (Value t')
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Value k
c Value t'
v Map (Value k) (Value t')
m, x
vx x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
cx x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
xs)) (Map (Value k) (Value t')
forall k a. Map k a
M.empty, x
forall a. Monoid a => a
mempty) Map (Value k) (Value t')
vmap
        (v' :: Value t
v', x' :: x
x') = Value t -> (Value t, x)
forall (t' :: T). Value t' -> (Value t', x)
step (Value t -> (Value t, x)) -> Value t -> (Value t, x)
forall a b. (a -> b) -> a -> b
$ Map (Value k) (Value t') -> Value t
constructor Map (Value k) (Value t')
ms
      in
        (Value t
v', x
cxs x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
x')

-- | Specialization of 'dfsValue' for case when changing the value is
-- not required.
dfsFoldValue ::
  Monoid x =>
  (forall t'. Value t' -> x)
  -> Value t
  -> x
dfsFoldValue :: (forall (t' :: T). Value t' -> x) -> Value t -> x
dfsFoldValue f :: forall (t' :: T). Value t' -> x
f = (Value t, x) -> x
forall a b. (a, b) -> b
snd ((Value t, x) -> x) -> (Value t -> (Value t, x)) -> Value t -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (t' :: T). Value t' -> (Value t', x))
-> Value t -> (Value t, x)
forall (t :: T) x.
Monoid x =>
(forall (t' :: T). Value t' -> (Value t', x))
-> Value t -> (Value t, x)
dfsValue (\v :: Value t'
v -> (Value t'
v, Value t' -> x
forall (t' :: T). Value t' -> x
f Value t'
v))

-- | Specialization of 'dfsValue' which only modifies given value.
dfsModifyValue ::
  (forall t'. Value t' -> Value t')
  -> Value t
  -> Value t
dfsModifyValue :: (forall (t' :: T). Value t' -> Value t') -> Value t -> Value t
dfsModifyValue f :: forall (t' :: T). Value t' -> Value t'
f = (Value t, ()) -> Value t
forall a b. (a, b) -> a
fst ((Value t, ()) -> Value t)
-> (Value t -> (Value t, ())) -> Value t -> Value t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (t' :: T). Value t' -> (Value t', ()))
-> Value t -> (Value t, ())
forall (t :: T) x.
Monoid x =>
(forall (t' :: T). Value t' -> (Value t', x))
-> Value t -> (Value t, x)
dfsValue ((, ()) (Value t' -> (Value t', ()))
-> (Value t' -> Value t') -> Value t' -> (Value t', ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value t' -> Value t'
forall (t' :: T). Value t' -> Value t'
f)

-- | If value is a string, return the stored string.
isStringValue :: Value t -> Maybe MText
isStringValue :: Value t -> Maybe MText
isStringValue =
  \case
    VString str :: MText
str -> MText -> Maybe MText
forall a. a -> Maybe a
Just MText
str
    _ -> Maybe MText
forall a. Maybe a
Nothing

-- | If value is a bytestring, return the stored bytestring.
isBytesValue :: Value t -> Maybe ByteString
isBytesValue :: Value t -> Maybe ByteString
isBytesValue =
  \case
    VBytes bytes :: ByteString
bytes -> ByteString -> Maybe ByteString
forall a. a -> Maybe a
Just ByteString
bytes
    _ -> Maybe ByteString
forall a. Maybe a
Nothing

-- | Takes a selector which checks whether a value can be converted
-- to something. Recursively applies it to all values. Collects extracted
-- values in a list.
allAtomicValues ::
  forall t a. (forall t'. Value t' -> Maybe a) -> Value t -> [a]
allAtomicValues :: (forall (t' :: T). Value t' -> Maybe a) -> Value t -> [a]
allAtomicValues selector :: forall (t' :: T). Value t' -> Maybe a
selector = (forall (t' :: T). Value t' -> [a]) -> Value t -> [a]
forall x (t :: T).
Monoid x =>
(forall (t' :: T). Value t' -> x) -> Value t -> x
dfsFoldValue (Maybe a -> [a]
forall a. Maybe a -> [a]
maybeToList (Maybe a -> [a]) -> (Value t' -> Maybe a) -> Value t' -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value t' -> Maybe a
forall (t' :: T). Value t' -> Maybe a
selector)