-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

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

module Morley.Michelson.Typed.Util
  ( -- * Instruction analysis
    DfsSettings (..)
  , CtorEffectsApp (..)
  , dfsTraverseInstr
  , dfsFoldInstr
  , dfsModifyInstr

  , isMichelsonInstr

  -- * Changing instruction tree structure
  , linearizeLeft
  , linearizeLeftDeep

  -- * Value analysis
  , dfsFoldMapValue
  , dfsFoldMapValueM
  , dfsMapValue
  , dfsTraverseValue
  , isStringValue
  , isBytesValue
  , allAtomicValues

  -- * Instruction generation
  , PushableStorageSplit (..)
  , splitPushableStorage

  -- * Working with 'RemFail'
  , analyzeInstrFailure

  -- * Annotations
  , SomeAnns(..)
  , instrAnns
  ) where

import Debug qualified (show)
import Prelude hiding (Ordering(..))

import Control.Monad.Writer.Strict (Writer, execWriterT, runWriter, tell, writer)
import Data.Constraint (Dict(..))
import Data.Default (Default(..))
import Data.Map qualified as M
import Data.Set qualified as S
import Data.Text.Internal.Builder (fromText)
import Fmt (Buildable(..))

import Morley.Michelson.Text (MText)
import Morley.Michelson.Typed.Aliases
import Morley.Michelson.Typed.Annotation
import Morley.Michelson.Typed.Contract
import Morley.Michelson.Typed.Instr
import Morley.Michelson.Typed.Scope
import Morley.Michelson.Typed.T qualified as T
import Morley.Michelson.Typed.Value
import Morley.Michelson.Typed.View
import Morley.Michelson.Untyped (AnyAnn)

-- $setup
-- >>> :m + Morley.Michelson.Typed.Instr

-- | Options for 'dfsTraverseInstr' family of functions.
data DfsSettings m = DfsSettings
  { forall (m :: * -> *). DfsSettings m -> Bool
dsGoToValues :: Bool
    -- ^ Whether @dfsTraverseInstr@ function should go into values which contain other
    -- instructions: lambdas and constant contracts
    -- (which can be passed to @CREATE_CONTRACT@).
  , forall (m :: * -> *). DfsSettings m -> CtorEffectsApp m
dsCtorEffectsApp :: CtorEffectsApp m
    -- ^ How do we handle intermediate nodes in instruction tree.
  , forall (m :: * -> *).
DfsSettings m
-> forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsInstrStep :: (forall i o. Instr i o -> m (Instr i o))
  , forall (m :: * -> *).
DfsSettings m -> forall (t' :: T). Value t' -> m (Value t')
dsValueStep :: (forall t'. Value t' -> m (Value t'))
  }

-- | Describes how intermediate nodes in instruction tree are accounted.
data CtorEffectsApp m = CtorEffectsApp
  { forall (m :: * -> *). CtorEffectsApp m -> Text
ceaName :: Text
    -- ^ Name of this way.
  , forall (m :: * -> *).
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
   Monad m =>
   Instr i o -> m (Instr i o) -> m (Instr i o)
ceaPostStep
      :: forall i o. Monad m
      => Instr i o
      -> m (Instr i o)
      -> m (Instr i o)
    -- ^ This transformation is applied after the step.
    -- It will be provided with the old instruction and the action gathered
    -- with the recursive traversal for the instruction subtree,
    -- and the result will go to the parent node.
  }

instance Buildable (CtorEffectsApp x) where
  build :: CtorEffectsApp x -> Builder
build CtorEffectsApp{Text
forall (i :: [T]) (o :: [T]).
Monad x =>
Instr i o -> x (Instr i o) -> x (Instr i o)
ceaPostStep :: forall (i :: [T]) (o :: [T]).
Monad x =>
Instr i o -> x (Instr i o) -> x (Instr i o)
ceaName :: Text
ceaPostStep :: forall (m :: * -> *).
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
   Monad m =>
   Instr i o -> m (Instr i o) -> m (Instr i o)
ceaName :: forall (m :: * -> *). CtorEffectsApp m -> Text
..} = Text -> Builder
fromText Text
ceaName

instance (Applicative x) => Default (DfsSettings x) where
  def :: DfsSettings x
def = DfsSettings :: forall (m :: * -> *).
Bool
-> CtorEffectsApp m
-> (forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o))
-> (forall (t' :: T). Value t' -> m (Value t'))
-> DfsSettings m
DfsSettings
    { dsGoToValues :: Bool
dsGoToValues = Bool
False
    , dsCtorEffectsApp :: CtorEffectsApp x
dsCtorEffectsApp = CtorEffectsApp :: forall (m :: * -> *).
Text
-> (forall (i :: [T]) (o :: [T]).
    Monad m =>
    Instr i o -> m (Instr i o) -> m (Instr i o))
-> CtorEffectsApp m
CtorEffectsApp
        { ceaName :: Text
ceaName = Text
"Do nothing"
        , ceaPostStep :: forall (i :: [T]) (o :: [T]).
Monad x =>
Instr i o -> x (Instr i o) -> x (Instr i o)
ceaPostStep = (x (Instr i o) -> x (Instr i o))
-> Instr i o -> x (Instr i o) -> x (Instr i o)
forall a b. a -> b -> a
const x (Instr i o) -> x (Instr i o)
forall a. a -> a
id
        }
    , dsInstrStep :: forall (i :: [T]) (o :: [T]). Instr i o -> x (Instr i o)
dsInstrStep = forall (i :: [T]) (o :: [T]). Instr i o -> x (Instr i o)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    , dsValueStep :: forall (t' :: T). Value t' -> x (Value t')
dsValueStep = forall (t' :: T). Value t' -> x (Value t')
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    }

-- | Traverse a typed instruction in depth-first order.
--
-- The 'dsInstrStep' and 'dsValueStep' actions will be applied in bottom-to-top order, i.e.
-- first to the children of a node, then to the node itself.
dfsTraverseInstr ::
     forall m inp out.
     (Monad m)
  => DfsSettings m
  -> Instr inp out
  -> m (Instr inp out)
dfsTraverseInstr :: forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr settings :: DfsSettings m
settings@DfsSettings{Bool
CtorEffectsApp m
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep :: forall (t' :: T). Value t' -> m (Value t')
dsInstrStep :: forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsCtorEffectsApp :: CtorEffectsApp m
dsGoToValues :: Bool
dsValueStep :: forall (m :: * -> *).
DfsSettings m -> forall (t' :: T). Value t' -> m (Value t')
dsInstrStep :: forall (m :: * -> *).
DfsSettings m
-> forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsCtorEffectsApp :: forall (m :: * -> *). DfsSettings m -> CtorEffectsApp m
dsGoToValues :: forall (m :: * -> *). DfsSettings m -> Bool
..} Instr inp out
i =
  case Instr inp out
i of
    Seq Instr inp b
i1 Instr b out
i2 -> (Instr inp b -> Instr b out -> Instr inp out)
-> Instr inp b -> Instr b out -> m (Instr inp out)
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 -> m (Instr i o)
recursion2 Instr inp b -> Instr b out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr inp b
i1 Instr b out
i2
    WithLoc ErrorSrcPos
loc Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 (ErrorSrcPos -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
ErrorSrcPos -> Instr inp out -> Instr inp out
WithLoc ErrorSrcPos
loc) Instr inp out
i1
    Meta SomeMeta
meta Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 (SomeMeta -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
SomeMeta -> Instr inp out -> Instr inp out
Meta SomeMeta
meta) Instr inp out
i1
    FrameInstr Proxy s
p Instr a b
i1 -> (Instr a b -> Instr inp out) -> Instr a b -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
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 Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
Nested Instr inp out
i1
    DocGroup DocGrouping
dg Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
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 Instr s out
i1 Instr (a : s) out
i2 -> (Instr s out -> Instr (a : s) out -> Instr ('TOption a : s) out)
-> Instr s out
-> Instr (a : s) out
-> m (Instr ('TOption a : s) out)
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 -> m (Instr i o)
recursion2 Instr s out -> Instr (a : s) out -> Instr ('TOption a : s) out
forall (s :: [T]) (out :: [T]) (a :: T).
Instr s out -> Instr (a : s) out -> Instr ('TOption a : s) out
IF_NONE Instr s out
i1 Instr (a : s) out
i2
    IF_LEFT Instr (a : s) out
i1 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
-> m (Instr ('TOr a b : s) out)
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 -> m (Instr i o)
recursion2 Instr (a : s) out -> Instr (b : s) out -> Instr ('TOr a b : s) out
forall (a :: T) (s :: [T]) (out :: [T]) (b :: T).
Instr (a : s) out -> Instr (b : s) out -> Instr ('TOr a b : s) out
IF_LEFT Instr (a : s) out
i1 Instr (b : s) out
i2
    IF_CONS Instr (a : 'TList a : s) out
i1 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
-> m (Instr ('TList a : s) out)
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 -> m (Instr i o)
recursion2 Instr (a : 'TList a : s) out
-> Instr s out -> Instr ('TList a : s) out
forall (a :: T) (s :: [T]) (out :: [T]).
Instr (a : 'TList a : s) out
-> Instr s out -> Instr ('TList a : s) out
IF_CONS Instr (a : 'TList a : s) out
i1 Instr s out
i2
    IF Instr s out
i1 Instr s out
i2 -> (Instr s out -> Instr s out -> Instr ('TBool : s) out)
-> Instr s out -> Instr s out -> m (Instr ('TBool : s) out)
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 -> m (Instr i o)
recursion2 Instr s out -> Instr s out -> Instr ('TBool : s) out
forall (s :: [T]) (out :: [T]).
Instr s out -> Instr s out -> Instr ('TBool : s) out
IF Instr s out
i1 Instr s out
i2
    AnnMAP AnnVar
ann Instr (MapOpInp c : s) (b : s)
i1 -> (Instr (MapOpInp c : s) (b : s) -> Instr (c : s) out)
-> Instr (MapOpInp c : s) (b : s) -> m (Instr (c : s) out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 (AnnVar
-> Instr (MapOpInp c : s) (b : s)
-> Instr (c : s) (MapOpRes c b : s)
forall (c :: T) (b :: T) (s :: [T]).
(MapOp c, SingI b) =>
AnnVar
-> Instr (MapOpInp c : s) (b : s)
-> Instr (c : s) (MapOpRes c b : s)
AnnMAP AnnVar
ann) Instr (MapOpInp c : s) (b : s)
i1
    ITER Instr (IterOpEl c : out) out
i1 -> (Instr (IterOpEl c : out) out -> Instr (c : out) out)
-> Instr (IterOpEl c : out) out -> m (Instr (c : out) out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 Instr (IterOpEl c : out) out -> Instr (c : out) out
forall (c :: T) (out :: [T]).
IterOp c =>
Instr (IterOpEl c : out) out -> Instr (c : out) out
ITER Instr (IterOpEl c : out) out
i1
    LOOP Instr out ('TBool : out)
i1 -> (Instr out ('TBool : out) -> Instr ('TBool : out) out)
-> Instr out ('TBool : out) -> m (Instr ('TBool : out) out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 Instr out ('TBool : out) -> Instr ('TBool : out) out
forall (out :: [T]).
Instr out ('TBool : out) -> Instr ('TBool : out) out
LOOP Instr out ('TBool : out)
i1
    LOOP_LEFT 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) -> m (Instr ('TOr a b : s) (b : s))
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
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 Instr a c
i1 -> (Instr a c -> Instr (b : a) (b : c))
-> Instr a c -> m (Instr (b : a) (b : c))
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
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 PeanoNatural n
s Instr s s'
i1 -> (Instr s s' -> Instr inp out) -> Instr s s' -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 (PeanoNatural n -> Instr s s' -> Instr inp out
forall (n :: Peano) (inp :: [T]) (out :: [T]) (s :: [T])
       (s' :: [T]).
ConstraintDIPN n inp out s s' =>
PeanoNatural n -> Instr s s' -> Instr inp out
DIPN PeanoNatural 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).
    AnnPUSH Anns '[VarAnn, Notes t]
ann Value' Instr t
v
      | Bool
dsGoToValues -> CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
   Monad m =>
   Instr i o -> m (Instr i o) -> m (Instr i o)
forall (m :: * -> *).
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
   Monad m =>
   Instr i o -> m (Instr i o) -> m (Instr i o)
ceaPostStep CtorEffectsApp m
dsCtorEffectsApp Instr inp out
i do
        Value' Instr t
innerV <- DfsSettings m -> Value' Instr t -> m (Value' Instr t)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
settings Value' Instr t
v
        Instr inp (t : inp) -> m (Instr inp (t : inp))
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsInstrStep (Instr inp (t : inp) -> m (Instr inp (t : inp)))
-> Instr inp (t : inp) -> m (Instr inp (t : inp))
forall a b. (a -> b) -> a -> b
$ Anns '[VarAnn, Notes t] -> Value' Instr t -> Instr inp (t : inp)
forall (t :: T) (inp :: [T]).
ConstantScope t =>
Anns '[VarAnn, Notes t] -> Value' Instr t -> Instr inp (t : inp)
AnnPUSH Anns '[VarAnn, Notes t]
ann Value' Instr t
innerV
     | Bool
otherwise -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i

    AnnLAMBDA Anns '[VarAnn, Notes i, Notes o]
ann (VLam RemFail Instr '[inp] '[out]
i1)
      | Bool
dsGoToValues ->
          (Instr '[i] '[o] -> Instr inp ('TLambda i o : inp))
-> Instr '[i] '[o] -> m (Instr inp ('TLambda i o : inp))
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 (Anns '[VarAnn, Notes i, Notes o]
-> Value' Instr ('TLambda i o) -> Instr inp ('TLambda i o : inp)
forall (i :: T) (o :: T) (inp :: [T]).
(SingI i, SingI o) =>
Anns '[VarAnn, Notes i, Notes o]
-> Value' Instr ('TLambda i o) -> Instr inp ('TLambda i o : inp)
AnnLAMBDA Anns '[VarAnn, Notes i, Notes o]
ann (Value' Instr ('TLambda i o) -> Instr inp ('TLambda i o : inp))
-> (Instr '[i] '[o] -> Value' Instr ('TLambda i o))
-> Instr '[i] '[o]
-> Instr inp ('TLambda i o : inp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RemFail Instr '[i] '[o] -> Value' Instr ('TLambda i o)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI 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 '[i] '[o] -> Value' Instr ('TLambda i o))
-> (Instr '[i] '[o] -> RemFail Instr '[i] '[o])
-> Instr '[i] '[o]
-> Value' Instr ('TLambda i o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr '[i] '[o] -> RemFail Instr '[i] '[o]
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 -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnCREATE_CONTRACT Anns '[VarAnn, VarAnn]
ann Contract' Instr p g
contract
      | Bool
dsGoToValues ->
          CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
   Monad m =>
   Instr i o -> m (Instr i o) -> m (Instr i o)
forall (m :: * -> *).
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
   Monad m =>
   Instr i o -> m (Instr i o) -> m (Instr i o)
ceaPostStep CtorEffectsApp m
dsCtorEffectsApp Instr inp out
i
            case Contract' Instr p g -> ContractCode' Instr p g
forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> ContractCode' instr cp st
cCode Contract' Instr p g
contract of
              ContractCode Instr (ContractInp p g) (ContractOut g)
c -> do
                Instr (ContractInp p g) (ContractOut g)
codeI <- DfsSettings m
-> Instr (ContractInp p g) (ContractOut g)
-> m (Instr (ContractInp p g) (ContractOut g))
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings m
settings Instr (ContractInp p g) (ContractOut g)
c
                [SomeView' Instr g]
viewsI <- [SomeView' Instr g]
-> (SomeView' Instr g -> m (SomeView' Instr g))
-> m [SomeView' Instr g]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (ViewsSet' Instr g -> [Element (ViewsSet' Instr g)]
forall t. Container t => t -> [Element t]
toList (ViewsSet' Instr g -> [Element (ViewsSet' Instr g)])
-> ViewsSet' Instr g -> [Element (ViewsSet' Instr g)]
forall a b. (a -> b) -> a -> b
$ Contract' Instr p g -> ViewsSet' Instr g
forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> ViewsSet' instr st
cViews Contract' Instr p g
contract) \(SomeView View' Instr arg g ret
v) -> do
                    Instr '[ 'TPair arg g] '[ret]
code <- DfsSettings m
-> Instr '[ 'TPair arg g] '[ret]
-> m (Instr '[ 'TPair arg g] '[ret])
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings m
settings (Instr '[ 'TPair arg g] '[ret]
 -> m (Instr '[ 'TPair arg g] '[ret]))
-> Instr '[ 'TPair arg g] '[ret]
-> m (Instr '[ 'TPair arg g] '[ret])
forall a b. (a -> b) -> a -> b
$ View' Instr arg g ret -> Instr '[ 'TPair arg g] '[ret]
forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> ViewCode' instr arg st ret
vCode View' Instr arg g ret
v
                    return $ View' Instr arg g ret -> SomeView' Instr g
forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> SomeView' instr st
SomeView View' Instr arg g ret
v{ vCode :: Instr '[ 'TPair arg g] '[ret]
vCode = Instr '[ 'TPair arg g] '[ret]
code }
                Instr
  ('TOption 'TKeyHash : 'TMutez : g : s)
  ('TOperation : 'TAddress : s)
-> m (Instr
        ('TOption 'TKeyHash : 'TMutez : g : s)
        ('TOperation : 'TAddress : s))
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsInstrStep (Instr
   ('TOption 'TKeyHash : 'TMutez : g : s)
   ('TOperation : 'TAddress : s)
 -> m (Instr
         ('TOption 'TKeyHash : 'TMutez : g : s)
         ('TOperation : 'TAddress : s)))
-> Instr
     ('TOption 'TKeyHash : 'TMutez : g : s)
     ('TOperation : 'TAddress : s)
-> m (Instr
        ('TOption 'TKeyHash : 'TMutez : g : s)
        ('TOperation : 'TAddress : s))
forall a b. (a -> b) -> a -> b
$ Anns '[VarAnn, VarAnn]
-> Contract' Instr p g
-> Instr
     ('TOption 'TKeyHash : 'TMutez : g : s)
     ('TOperation : 'TAddress : s)
forall (p :: T) (g :: T) (s :: [T]).
(ParameterScope p, StorageScope g, IsNotInView) =>
Anns '[VarAnn, VarAnn]
-> Contract' Instr p g
-> Instr
     ('TOption 'TKeyHash : 'TMutez : g : s)
     ('TOperation : 'TAddress : s)
AnnCREATE_CONTRACT Anns '[VarAnn, VarAnn]
ann (Contract' Instr p g
 -> Instr
      ('TOption 'TKeyHash : 'TMutez : g : s)
      ('TOperation : 'TAddress : s))
-> Contract' Instr p g
-> Instr
     ('TOption 'TKeyHash : 'TMutez : g : s)
     ('TOperation : 'TAddress : s)
forall a b. (a -> b) -> a -> b
$ Contract' Instr p g
contract
                  { cCode :: ContractCode' Instr p g
cCode = Instr (ContractInp p g) (ContractOut g) -> ContractCode' Instr p g
forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
instr (ContractInp cp st) (ContractOut st)
-> ContractCode' instr cp st
ContractCode Instr (ContractInp p g) (ContractOut g)
codeI
                  , cViews :: ViewsSet' Instr g
cViews = (Seq $ SomeView' Instr g) -> ViewsSet' Instr g
forall (instr :: [T] -> [T] -> *) (st :: T).
(Seq $ SomeView' instr st) -> ViewsSet' instr st
UnsafeViewsSet ((Seq $ SomeView' Instr g) -> ViewsSet' Instr g)
-> (Seq $ SomeView' Instr g) -> ViewsSet' Instr g
forall a b. (a -> b) -> a -> b
$ [ListElement (Seq $ SomeView' Instr g)] -> Seq $ SomeView' Instr g
forall l. (FromList l, FromListC l) => [ListElement l] -> l
fromList [ListElement (Seq $ SomeView' Instr g)]
[SomeView' Instr g]
viewsI
                  }
      | Bool
otherwise -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i

    Nop{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    Ext (TEST_ASSERT (TestAssert Text
nm PrintComment inp
pc Instr inp ('TBool : out)
i1)) ->
      (Instr inp ('TBool : out) -> Instr inp inp)
-> Instr inp ('TBool : out) -> m (Instr inp inp)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 (ExtInstr inp -> Instr inp inp
forall (inp :: [T]). ExtInstr inp -> Instr inp inp
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 (s :: [T]) (out :: [T]).
Text -> PrintComment s -> Instr s ('TBool : out) -> TestAssert s
TestAssert Text
nm PrintComment inp
pc) Instr inp ('TBool : out)
i1
    Ext{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnCAR{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnCDR{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    DROP{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    DROPN{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnDUP{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnDUPN{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    SWAP{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    DIG{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    DUG{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnSOME{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnNONE{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnUNIT{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnPAIR{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnUNPAIR{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnPAIRN{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    UNPAIRN{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnLEFT{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnRIGHT{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnNIL{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnCONS{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnSIZE{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnEMPTY_SET{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnEMPTY_MAP{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnEMPTY_BIG_MAP{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnMEM{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnGET{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnGETN{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnUPDATE{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnUPDATEN{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnGET_AND_UPDATE{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnEXEC{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnAPPLY{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    FAILWITH{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnCAST{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnRENAME{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnPACK{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnUNPACK{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnCONCAT{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnCONCAT'{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnSLICE{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnISNAT{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnADD{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnSUB{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnSUB_MUTEZ{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnMUL{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnEDIV{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnABS{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnNEG{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnLSL{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnLSR{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnOR{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnAND{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnXOR{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnNOT{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnCOMPARE{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnEQ{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnNEQ{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnLT{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnGT{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnLE{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnGE{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnINT{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnVIEW{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnSELF{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnCONTRACT{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnTRANSFER_TOKENS{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnSET_DELEGATE{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnIMPLICIT_ACCOUNT{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnNOW{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnAMOUNT{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnBALANCE{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnVOTING_POWER{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnTOTAL_VOTING_POWER{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnCHECK_SIGNATURE{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnSHA256{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnSHA512{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnBLAKE2B{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnSHA3{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnKECCAK{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnHASH_KEY{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnPAIRING_CHECK{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnSOURCE{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnSENDER{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnADDRESS{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnCHAIN_ID{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnLEVEL{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnSELF_ADDRESS{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    NEVER{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnTICKET{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnREAD_TICKET{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnSPLIT_TICKET{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnJOIN_TICKETS{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnOPEN_CHEST{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnSAPLING_EMPTY_STATE{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnSAPLING_VERIFY_UPDATE{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnMIN_BLOCK_TIME{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
    AnnEMIT{} -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
  where
    recursion0 ::
      forall a b. Instr a b -> m (Instr a b)
    recursion0 :: forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr a b
i0 =
      CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
   Monad m =>
   Instr i o -> m (Instr i o) -> m (Instr i o)
forall (m :: * -> *).
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
   Monad m =>
   Instr i o -> m (Instr i o) -> m (Instr i o)
ceaPostStep CtorEffectsApp m
dsCtorEffectsApp Instr a b
i0 (m (Instr a b) -> m (Instr a b)) -> m (Instr a b) -> m (Instr a b)
forall a b. (a -> b) -> a -> b
$
      Instr a b -> m (Instr a b)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsInstrStep Instr a b
i0

    recursion1 ::
      forall a b c d. (Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
    recursion1 :: forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 Instr a b -> Instr c d
constructor Instr a b
i0 =
      CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
   Monad m =>
   Instr i o -> m (Instr i o) -> m (Instr i o)
forall (m :: * -> *).
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
   Monad m =>
   Instr i o -> m (Instr i o) -> m (Instr i o)
ceaPostStep CtorEffectsApp m
dsCtorEffectsApp (Instr a b -> Instr c d
constructor Instr a b
i0) do
        Instr a b
innerI <- DfsSettings m -> Instr a b -> m (Instr a b)
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings m
settings Instr a b
i0
        Instr c d -> m (Instr c d)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsInstrStep (Instr c d -> m (Instr c d)) -> Instr c d -> m (Instr c d)
forall a b. (a -> b) -> a -> b
$ Instr a b -> Instr c d
constructor Instr a b
innerI

    recursion2 ::
      forall i o i1 o1 i2 o2.
      (Instr i1 o1 -> Instr i2 o2 -> Instr i o) ->
      Instr i1 o1 -> Instr i2 o2 -> m (Instr i o)
    recursion2 :: 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 -> m (Instr i o)
recursion2 Instr i1 o1 -> Instr i2 o2 -> Instr i o
constructor Instr i1 o1
i1 Instr i2 o2
i2 =
      CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
   Monad m =>
   Instr i o -> m (Instr i o) -> m (Instr i o)
forall (m :: * -> *).
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
   Monad m =>
   Instr i o -> m (Instr i o) -> m (Instr i o)
ceaPostStep CtorEffectsApp m
dsCtorEffectsApp (Instr i1 o1 -> Instr i2 o2 -> Instr i o
constructor Instr i1 o1
i1 Instr i2 o2
i2) do
        Instr i1 o1
i1' <- DfsSettings m -> Instr i1 o1 -> m (Instr i1 o1)
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings m
settings Instr i1 o1
i1
        Instr i2 o2
i2' <- DfsSettings m -> Instr i2 o2 -> m (Instr i2 o2)
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings m
settings Instr i2 o2
i2
        Instr i o -> m (Instr i o)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsInstrStep (Instr i o -> m (Instr i o)) -> Instr i o -> m (Instr i o)
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'

-- | Specialization of 'dfsTraverseInstr' for case when changing the instruction is
-- not required.
dfsFoldInstr
  :: forall x inp out.
      (Monoid x)
  => DfsSettings (Writer x)
  -> (forall i o. Instr i o -> x)
  -> Instr inp out
  -> x
dfsFoldInstr :: forall x (inp :: [T]) (out :: [T]).
Monoid x =>
DfsSettings (Writer x)
-> (forall (i :: [T]) (o :: [T]). Instr i o -> x)
-> Instr inp out
-> x
dfsFoldInstr DfsSettings (Writer x)
settings forall (i :: [T]) (o :: [T]). Instr i o -> x
step =
  (Instr inp out, x) -> x
forall a b. (a, b) -> b
snd ((Instr inp out, x) -> x)
-> (Instr inp out -> (Instr inp out, x)) -> Instr inp out -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Writer x (Instr inp out) -> (Instr inp out, x)
forall w a. Writer w a -> (a, w)
runWriter (Writer x (Instr inp out) -> (Instr inp out, x))
-> (Instr inp out -> Writer x (Instr inp out))
-> Instr inp out
-> (Instr inp out, x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DfsSettings (Writer x) -> Instr inp out -> Writer x (Instr inp out)
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings (Writer x)
settings{dsInstrStep :: forall (i :: [T]) (o :: [T]). Instr i o -> Writer x (Instr i o)
dsInstrStep = (Instr i o, x) -> Writer x (Instr i o)
forall w (m :: * -> *) a. MonadWriter w m => (a, w) -> m a
writer ((Instr i o, x) -> Writer x (Instr i o))
-> (Instr i o -> (Instr i o, x))
-> Instr i o
-> Writer x (Instr i o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Instr i o -> Instr i o
forall a. a -> a
id (Instr i o -> Instr i o)
-> (Instr i o -> x) -> Instr i o -> (Instr i o, x)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Instr i o -> x
forall (i :: [T]) (o :: [T]). Instr i o -> x
step)}

-- | Specialization of 'dfsTraverseInstr' which only modifies given instruction.
dfsModifyInstr
  :: DfsSettings Identity
  -> (forall i o. Instr i o -> Instr i o)
  -> Instr inp out
  -> Instr inp out
dfsModifyInstr :: forall (inp :: [T]) (out :: [T]).
DfsSettings Identity
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
dfsModifyInstr DfsSettings Identity
settings forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
step =
  Identity (Instr inp out) -> Instr inp out
forall a. Identity a -> a
runIdentity (Identity (Instr inp out) -> Instr inp out)
-> (Instr inp out -> Identity (Instr inp out))
-> Instr inp out
-> Instr inp out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DfsSettings Identity -> Instr inp out -> Identity (Instr inp out)
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings Identity
settings{dsInstrStep :: forall (i :: [T]) (o :: [T]). Instr i o -> Identity (Instr i o)
dsInstrStep = (Instr i o -> Identity (Instr i o)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Instr i o -> Identity (Instr i o))
-> (Instr i o -> Instr i o) -> Instr i o -> Identity (Instr i o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr i o -> Instr i o
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
step)}

-- | 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 :: forall (i :: [T]) (o :: [T]).
HasCallStack =>
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 :: forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go = \case
    WithLoc ErrorSrcPos
loc 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 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 (ErrorSrcPos -> Instr i o -> Instr i o
forall (inp :: [T]) (out :: [T]).
ErrorSrcPos -> Instr inp out -> Instr inp out
WithLoc ErrorSrcPos
loc Instr i o
i0)
      RemFail Instr i o
r -> RemFail Instr i o
r
    Meta SomeMeta
meta 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 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 (SomeMeta -> Instr i o -> Instr i o
forall (inp :: [T]) (out :: [T]).
SomeMeta -> Instr inp out -> Instr inp out
Meta SomeMeta
meta Instr i o
i0)
      RemFail Instr i o
r -> RemFail Instr i o
r
    FrameInstr Proxy s
s 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 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 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
$ Text
"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
Debug.show Instr a Any
forall (o' :: [T]). Instr a o'
i0
    Seq Instr i b
a Instr b o
b -> Instr i b -> Instr b o' -> Instr i o'
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
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
    Instr i o
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 (inp :: [T]). Instr inp inp
Nop
    Ext 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 (inp :: [T]). ExtInstr inp -> Instr inp inp
Ext ExtInstr i
e)
    Nested 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 DocGrouping
g 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 Instr s o
l 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]) (out :: [T]) (a :: T).
Instr s out -> Instr (a : s) out -> Instr ('TOption a : s) out
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 Instr (a : s) o
l 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]) (out :: [T]) (b :: T).
Instr (a : s) out -> Instr (b : s) out -> Instr ('TOr a b : s) out
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 Instr (a : 'TList a : s) o
l 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]) (out :: [T]).
Instr (a : 'TList a : s) out
-> Instr s out -> Instr ('TList a : s) out
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 Instr s o
l 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]) (out :: [T]).
Instr s out -> Instr s out -> Instr ('TBool : s) out
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@AnnMAP{} -> 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@AnnLAMBDA{} -> 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@AnnDUP{} -> 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@AnnDUPN{} -> 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@AnnPUSH{} -> 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@AnnSOME{} -> 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@AnnNONE{} -> 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@AnnUNIT{} -> 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@AnnUNPAIR{} -> 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@AnnPAIRN{} -> 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@UNPAIRN{} -> 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@AnnLEFT{} -> 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@AnnRIGHT{} -> 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@AnnNIL{} -> 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@AnnCONS{} -> 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@AnnSIZE{} -> 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@AnnEMPTY_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@AnnEMPTY_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@AnnEMPTY_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@AnnMEM{} -> 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@AnnGET{} -> 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@AnnGETN{} -> 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@AnnUPDATE{} -> 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@AnnUPDATEN{} -> 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@AnnGET_AND_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@AnnEXEC{} -> 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@AnnAPPLY{} -> 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
    Instr i o
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]) (out :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : s) out
FAILWITH
    i :: Instr i o
i@AnnCAST{} -> 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@AnnRENAME{} -> 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@AnnPACK{} -> 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@AnnUNPACK{} -> 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@AnnCONCAT{} -> 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@AnnCONCAT'{} -> 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@AnnSLICE{} -> 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@AnnISNAT{} -> 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@AnnADD{} -> 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@AnnSUB{} -> 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@AnnSUB_MUTEZ{} -> 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@AnnMUL{} -> 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@AnnEDIV{} -> 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@AnnABS{} -> 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@AnnNEG{} -> 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@AnnLSL{} -> 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@AnnLSR{} -> 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@AnnOR{} -> 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@AnnAND{} -> 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@AnnXOR{} -> 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@AnnNOT{} -> 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@AnnCOMPARE{} -> 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@AnnEQ{} -> 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@AnnNEQ{} -> 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@AnnLT{} -> 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@AnnGT{} -> 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@AnnLE{} -> 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@AnnGE{} -> 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@AnnINT{} -> 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@AnnVIEW{} -> 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@AnnSELF{} -> 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@AnnCONTRACT{} -> 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@AnnTRANSFER_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@AnnSET_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@AnnCREATE_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@AnnIMPLICIT_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@AnnNOW{} -> 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@AnnAMOUNT{} -> 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@AnnBALANCE{} -> 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@AnnVOTING_POWER{} -> 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@AnnTOTAL_VOTING_POWER{} -> 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@AnnCHECK_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@AnnSHA256{} -> 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@AnnSHA512{} -> 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@AnnBLAKE2B{} -> 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@AnnSHA3{} -> 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@AnnKECCAK{} -> 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@AnnHASH_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@AnnPAIRING_CHECK{} -> 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@AnnSOURCE{} -> 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@AnnSENDER{} -> 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@AnnADDRESS{} -> 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@AnnCHAIN_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@AnnLEVEL{} -> 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@AnnSELF_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
    Instr i o
NEVER -> (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 (s :: [T]) (out :: [T]). Instr ('TNever : s) out
NEVER
    i :: Instr i o
i@AnnTICKET{} -> 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@AnnREAD_TICKET{} -> 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@AnnSPLIT_TICKET{} -> 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@AnnJOIN_TICKETS{} -> 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@AnnOPEN_CHEST{} -> 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@AnnSAPLING_EMPTY_STATE{} -> 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@AnnSAPLING_VERIFY_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@AnnMIN_BLOCK_TIME{} -> 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@AnnEMIT{} -> 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
-- v'Seq' have a single instruction (i. e. not v'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 :: forall (inp :: [T]) (out :: [T]). 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 :: forall (inp :: [T]) (out :: [T]).
Bool -> Instr inp out -> Instr inp out
linearizeLeftHelper Bool
isLeftInstrAlreadyLinear =
      \case
        Seq Instr inp b
i1 (Seq Instr b b
i2 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 (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
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 (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
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 Instr inp b
i1 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 (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
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 (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
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
        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 :: forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
linearizeLeftDeep = DfsSettings Identity
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
forall (inp :: [T]) (out :: [T]).
DfsSettings Identity
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
dfsModifyInstr DfsSettings Identity
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.
dfsMapValue ::
     forall t.
     DfsSettings Identity
  -> Value t
  -> Value t
dfsMapValue :: forall (t :: T). DfsSettings Identity -> Value t -> Value t
dfsMapValue DfsSettings Identity
settings Value t
v = Identity (Value t) -> Value t
forall a. Identity a -> a
runIdentity (Identity (Value t) -> Value t) -> Identity (Value t) -> Value t
forall a b. (a -> b) -> a -> b
$ DfsSettings Identity -> Value t -> Identity (Value t)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings Identity
settings Value t
v

-- | Traverse a value in depth-first order.
dfsTraverseValue ::
     forall t m.
     (Monad m)
  => DfsSettings m
  -> Value t
  -> m (Value t)
dfsTraverseValue :: forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue settings :: DfsSettings m
settings@DfsSettings{Bool
CtorEffectsApp m
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep :: forall (t' :: T). Value t' -> m (Value t')
dsInstrStep :: forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsCtorEffectsApp :: CtorEffectsApp m
dsGoToValues :: Bool
dsValueStep :: forall (m :: * -> *).
DfsSettings m -> forall (t' :: T). Value t' -> m (Value t')
dsInstrStep :: forall (m :: * -> *).
DfsSettings m
-> forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsCtorEffectsApp :: forall (m :: * -> *). DfsSettings m -> CtorEffectsApp m
dsGoToValues :: forall (m :: * -> *). DfsSettings m -> Bool
..} Value t
i = case Value t
i of
  -- Atomic
  VKey{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  Value t
VUnit -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VSignature{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VChainId{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VOp{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VContract{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VTicket{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i  -- cannot appear as constant in a contract
  VLam RemFail Instr '[inp] '[out]
lambda -> do
    Value' Instr ('TLambda inp out)
v <- (Instr '[inp] '[out] -> Value' Instr ('TLambda inp out))
-> m (Instr '[inp] '[out]) -> m (Value' Instr ('TLambda inp out))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RemFail Instr '[inp] '[out] -> Value' Instr ('TLambda inp out)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI 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) (m (Instr '[inp] '[out]) -> m (Value' Instr ('TLambda inp out)))
-> m (Instr '[inp] '[out]) -> m (Value' Instr ('TLambda inp out))
forall a b. (a -> b) -> a -> b
$ DfsSettings m -> Instr '[inp] '[out] -> m (Instr '[inp] '[out])
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings m
settings (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)
    Value' Instr ('TLambda inp out)
-> m (Value' Instr ('TLambda inp out))
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value' Instr ('TLambda inp out)
v
  VInt{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VNat{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VString{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VBytes{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VMutez{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VBool{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VKeyHash{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VBls12381Fr{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VBls12381G1{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VBls12381G2{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VTimestamp{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VAddress{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VChestKey{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VChest{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
  VTxRollupL2Address{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i

  -- Non-atomic
  VOption Maybe (Value' Instr t1)
mVal -> case Maybe (Value' Instr t1)
mVal of
    Maybe (Value' Instr t1)
Nothing -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
    Just Value' Instr t1
val -> (Value' Instr t1 -> Value t) -> Value' Instr t1 -> m (Value t)
forall (t' :: T). (Value t' -> Value t) -> Value t' -> m (Value t)
recursion1 (Maybe (Value' Instr t1) -> Value' Instr ('TOption t1)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption (Maybe (Value' Instr t1) -> Value' Instr ('TOption t1))
-> (Value' Instr t1 -> Maybe (Value' Instr t1))
-> Value' Instr t1
-> Value' Instr ('TOption t1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' Instr t1 -> Maybe (Value' Instr t1)
forall a. a -> Maybe a
Just) Value' Instr t1
val
  VList [Value' Instr t1]
vals -> do
    [Value' Instr t1]
vs <- (Value' Instr t1 -> m (Value' Instr t1))
-> [Value' Instr t1] -> m [Value' Instr t1]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (DfsSettings m -> Value' Instr t1 -> m (Value' Instr t1)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
settings) [Value' Instr t1]
vals
    Value ('TList t1) -> m (Value ('TList t1))
forall (t' :: T). Value t' -> m (Value t')
dsValueStep (Value ('TList t1) -> m (Value ('TList t1)))
-> Value ('TList t1) -> m (Value ('TList t1))
forall a b. (a -> b) -> a -> b
$ [Value' Instr t1] -> Value ('TList t1)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
VList [Value' Instr t1]
vs
  VSet Set (Value t1)
vals -> do
    Set (Value t1)
cs <- [Value t1] -> Set (Value t1)
forall a. Ord a => [a] -> Set a
S.fromList ([Value t1] -> Set (Value t1))
-> m [Value t1] -> m (Set (Value t1))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value t1 -> m (Value t1)) -> [Value t1] -> m [Value t1]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (DfsSettings m -> Value t1 -> m (Value t1)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
settings) (Set (Value t1) -> [Value t1]
forall a. Set a -> [a]
S.toList Set (Value t1)
vals)
    Value ('TSet t1) -> m (Value ('TSet t1))
forall (t' :: T). Value t' -> m (Value t')
dsValueStep (Set (Value t1) -> Value ('TSet t1)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
(SingI t1, Comparable t1) =>
Set (Value' instr t1) -> Value' instr ('TSet t1)
VSet Set (Value t1)
cs)
  VPair (Value' Instr l
v1, Value' Instr r
v2) -> do
    Value' Instr l
v1' <- DfsSettings m -> Value' Instr l -> m (Value' Instr l)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
settings Value' Instr l
v1
    Value' Instr r
v2' <- DfsSettings m -> Value' Instr r -> m (Value' Instr r)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
settings Value' Instr r
v2
    Value ('TPair l r) -> m (Value ('TPair l r))
forall (t' :: T). Value t' -> m (Value t')
dsValueStep (Value ('TPair l r) -> m (Value ('TPair l r)))
-> Value ('TPair l r) -> m (Value ('TPair l r))
forall a b. (a -> b) -> a -> b
$ (Value' Instr l, Value' Instr r) -> Value ('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 Either (Value' Instr l) (Value' Instr r)
vEither -> case Either (Value' Instr l) (Value' Instr r)
vEither of
    Left Value' Instr l
v -> (Value' Instr l -> Value t) -> Value' Instr l -> m (Value t)
forall (t' :: T). (Value t' -> Value t) -> Value t' -> m (Value t)
recursion1 (Either (Value' Instr l) (Value' Instr r) -> Value' Instr ('TOr l r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(SingI l, SingI 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 Value' Instr r
v -> (Value' Instr r -> Value t) -> Value' Instr r -> m (Value t)
forall (t' :: T). (Value t' -> Value t) -> Value t' -> m (Value t)
recursion1 (Either (Value' Instr l) (Value' Instr r) -> Value' Instr ('TOr l r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(SingI l, SingI 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 Map (Value' Instr k) (Value' Instr v)
vmap -> (Map (Value' Instr k) (Value' Instr v) -> Value t)
-> Map (Value' Instr k) (Value' Instr v) -> m (Value t)
forall (k :: T) (v :: T).
Comparable k =>
(Map (Value k) (Value v) -> Value t)
-> Map (Value k) (Value v) -> m (Value t)
mapRecursion Map (Value' Instr k) (Value' Instr v) -> Value t
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI k, SingI 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 Maybe Natural
bmId Map (Value' Instr k) (Value' Instr v)
vmap -> (Map (Value' Instr k) (Value' Instr v) -> Value t)
-> Map (Value' Instr k) (Value' Instr v) -> m (Value t)
forall (k :: T) (v :: T).
Comparable k =>
(Map (Value k) (Value v) -> Value t)
-> Map (Value k) (Value v) -> m (Value t)
mapRecursion (Maybe Natural
-> Map (Value' Instr k) (Value' Instr v)
-> Value' Instr ('TBigMap k v)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI k, SingI v, Comparable k, HasNoBigMap v) =>
Maybe Natural
-> Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
VBigMap Maybe Natural
bmId) Map (Value' Instr k) (Value' Instr v)
vmap
  where
    recursion1 ::
         forall t'.
         (Value t' -> Value t)
      -> Value t'
      -> m (Value t)
    recursion1 :: forall (t' :: T). (Value t' -> Value t) -> Value t' -> m (Value t)
recursion1 Value t' -> Value t
constructor Value t'
v = do
      Value t'
v' <- DfsSettings m -> Value t' -> m (Value t')
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
settings Value t'
v
      Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep (Value t -> m (Value t)) -> Value t -> m (Value t)
forall a b. (a -> b) -> a -> b
$ Value t' -> Value t
constructor Value t'
v'

    mapRecursion
      :: forall k v. Comparable k
      => (M.Map (Value k) (Value v) -> Value t)
      -> M.Map (Value k) (Value v)
      -> m (Value t)
    mapRecursion :: forall (k :: T) (v :: T).
Comparable k =>
(Map (Value k) (Value v) -> Value t)
-> Map (Value k) (Value v) -> m (Value t)
mapRecursion Map (Value k) (Value v) -> Value t
constructor Map (Value k) (Value v)
vmap = do
      Map (Value k) (Value v)
vmap' <-
        [(Value k, Value v)] -> Map (Value k) (Value v)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Value k, Value v)] -> Map (Value k) (Value v))
-> m [(Value k, Value v)] -> m (Map (Value k) (Value v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Value k, Value v)]
-> ((Value k, Value v) -> m (Value k, Value v))
-> m [(Value k, Value v)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map (Value k) (Value v) -> [(Value k, Value v)]
forall k a. Map k a -> [(k, a)]
M.toList Map (Value k) (Value v)
vmap) \(Value k
k, Value v
v) -> do
          Value k
k' <- DfsSettings m -> Value k -> m (Value k)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
settings Value k
k
          Value v
v' <- DfsSettings m -> Value v -> m (Value v)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
settings Value v
v
          pure (Value k
k', Value v
v')
      Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep (Value t -> m (Value t)) -> Value t -> m (Value t)
forall a b. (a -> b) -> a -> b
$ Map (Value k) (Value v) -> Value t
constructor Map (Value k) (Value v)
vmap'

-- | Specialization of 'dfsMapValue' for case when changing the value is
-- not required.
dfsFoldMapValue
  :: Monoid x
  => (forall t'. Value t' -> x)
  -> Value t
  -> x
dfsFoldMapValue :: forall x (t :: T).
Monoid x =>
(forall (t' :: T). Value t' -> x) -> Value t -> x
dfsFoldMapValue forall (t' :: T). Value t' -> x
step Value t
v =
  Identity x -> x
forall a. Identity a -> a
runIdentity (Identity x -> x) -> Identity x -> x
forall a b. (a -> b) -> a -> b
$ (forall (t' :: T). Value t' -> Identity x) -> Value t -> Identity x
forall x (m :: * -> *) (t :: T).
(Monoid x, Monad m) =>
(forall (t' :: T). Value t' -> m x) -> Value t -> m x
dfsFoldMapValueM (x -> Identity x
forall (f :: * -> *) a. Applicative f => a -> f a
pure (x -> Identity x) -> (Value t' -> x) -> Value t' -> Identity x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value t' -> x
forall (t' :: T). Value t' -> x
step) Value t
v

-- | Specialization of 'dfsMapValue' for case when changing the value is
-- not required.
dfsFoldMapValueM
  :: (Monoid x, Monad m)
  => (forall t'. Value t' -> m x)
  -> Value t
  -> m x
dfsFoldMapValueM :: forall x (m :: * -> *) (t :: T).
(Monoid x, Monad m) =>
(forall (t' :: T). Value t' -> m x) -> Value t -> m x
dfsFoldMapValueM forall (t' :: T). Value t' -> m x
step Value t
v = do
  WriterT x m (Value t) -> m x
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT (WriterT x m (Value t) -> m x) -> WriterT x m (Value t) -> m x
forall a b. (a -> b) -> a -> b
$
    DfsSettings (WriterT x m) -> Value t -> WriterT x m (Value t)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue
      (DfsSettings (WriterT x m)
forall a. Default a => a
def{ dsValueStep :: forall (t' :: T). Value t' -> WriterT x m (Value t')
dsValueStep =
        (\Value t'
val -> do
            x
x <- m x -> WriterT x m x
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m x -> WriterT x m x) -> m x -> WriterT x m x
forall a b. (a -> b) -> a -> b
$ Value t' -> m x
forall (t' :: T). Value t' -> m x
step Value t'
val
            x -> WriterT x m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell x
x
            pure Value t'
val
        )
      }) Value t
v

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

-- | If value is a bytestring, return the stored bytestring.
isBytesValue :: Value t -> Maybe ByteString
isBytesValue :: forall (t :: T). Value t -> Maybe ByteString
isBytesValue =
  \case
    VBytes ByteString
bytes -> ByteString -> Maybe ByteString
forall a. a -> Maybe a
Just ByteString
bytes
    Value t
_ -> 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) a.
(forall (t' :: T). Value t' -> Maybe a) -> Value t -> [a]
allAtomicValues 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
dfsFoldMapValue (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)


--------------------------------------------------------------------------------
-- Instruction generation
--------------------------------------------------------------------------------

-- | Result of splitting a storage 'Value' of @st@ on the stack @s@.
--
-- The idea behind this is to either: prove that the whole 'Value' can be put on
-- the stack without containing a single @big_map@ or to split it into:
-- a 'Value' containing its @big_map@s and an instruction to reconstruct the
-- storage.
--
-- The main idea behind this is to create a large storage in Michelson code to
-- then create a contract using @CREATE_CONTRACT@.
-- Note: a simpler solution would have been to replace @big_map@ 'Value's with
-- an 'EMPTY_BIG_MAP' followed by many 'UPDATE' to push its content, but sadly
-- a bug (tezos/tezos/1154) prevents this from being done.
data PushableStorageSplit s st where
  -- | The type of the storage is fully constant.
  ConstantStorage
    :: ConstantScope st
    => Value st
    -> PushableStorageSplit s st

  -- | The type of the storage is not a constant, but its value does not contain
  -- @big_map@s. E.g. A 'Right ()' value of type 'Either (BigMap k v) ()'.
  PushableValueStorage
    :: StorageScope st
    => Instr s (st ': s)
    -> PushableStorageSplit s st

  -- | The type of the storage and part of its value (here @heavy@) contain one or
  -- more @big_map@s or @ticket@s. The instruction can take the non-pushable
  -- 'Value heavy' and reconstruct the original 'Value st' without using any
  -- 'EMPTY_BIG_MAP'.
  PartlyPushableStorage
    :: (StorageScope heavy, StorageScope st)
    => Value heavy -> Instr (heavy ': s) (st ': s)
    -> PushableStorageSplit s st

-- | Splits the given storage 'Value' into a 'PushableStorageSplit'.
--
-- This is based off the fact that the only storages that cannot be directly
-- 'PUSH'ed are the ones that contain 'Morley.Michelson.Typed.Haskell.Value.BigMap's and tickets.
-- See difference between 'StorageScope' and 'ConstantScope'.
--
-- So what we do here is to create a 'Value' as small as possible with all the
-- @big_map@s in it (if any) and an 'Instr' that can use it to rebuild the original
-- storage 'Value'.
--
-- Note: This is done this way to avoid using 'EMPTY_BIG_MAP' instructions, see
-- 'PushableStorageSplit' for motivation.
splitPushableStorage :: StorageScope t => Value t -> PushableStorageSplit s t
splitPushableStorage :: forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage Value t
v = case Value t
v of
  -- Atomic (except op and contract)
  VKey{}        -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  Value t
VUnit         -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VSignature{}  -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VChainId{}    -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VLam{}       -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VInt{}        -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VNat{}        -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VString{}     -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VBytes{}      -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VMutez{}      -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VBool{}       -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VKeyHash{}    -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VBls12381Fr{} -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VBls12381G1{} -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VBls12381G2{} -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VTimestamp{}  -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VAddress{}    -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VChest{}      -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VChestKey{}   -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VTxRollupL2Address{} -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
  VTicket{}     -> Value t -> Instr (t : s) (t : s) -> PushableStorageSplit s t
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value t
v Instr (t : s) (t : s)
forall (inp :: [T]). Instr inp inp
Nop

  -- Non-atomic
  VOption (Maybe (Value t1)
Nothing :: Maybe (Value tm)) -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope tm) of
    Right Dict (ConstantScope t1)
Dict -> Value ('TOption t1) -> PushableStorageSplit s ('TOption t1)
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage (Value ('TOption t1) -> PushableStorageSplit s ('TOption t1))
-> Value ('TOption t1) -> PushableStorageSplit s ('TOption t1)
forall a b. (a -> b) -> a -> b
$ Maybe (Value t1) -> Value ('TOption t1)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption Maybe (Value t1)
forall a. Maybe a
Nothing
    Left BadTypeForScope
_     -> Instr s (t : s) -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage Instr s (t : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ s, out ~ ('TOption a : s), SingI a) =>
Instr inp out
NONE
  VOption (Just Value t1
jVal :: Maybe (Value tm)) -> case Value t1 -> PushableStorageSplit s t1
forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage Value t1
jVal of
    ConstantStorage Value t1
_ -> Value ('TOption t1) -> PushableStorageSplit s ('TOption t1)
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage (Value ('TOption t1) -> PushableStorageSplit s ('TOption t1))
-> (Maybe (Value t1) -> Value ('TOption t1))
-> Maybe (Value t1)
-> PushableStorageSplit s ('TOption t1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Value t1) -> Value ('TOption t1)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption (Maybe (Value t1) -> PushableStorageSplit s ('TOption t1))
-> Maybe (Value t1) -> PushableStorageSplit s ('TOption t1)
forall a b. (a -> b) -> a -> b
$ Value t1 -> Maybe (Value t1)
forall a. a -> Maybe a
Just Value t1
jVal
    PushableValueStorage Instr s (t1 : s)
instr -> Instr s (t : s) -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr s (t : s) -> PushableStorageSplit s t)
-> Instr s (t : s) -> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ Instr s (t1 : s)
instr Instr s (t1 : s) -> Instr (t1 : s) (t : s) -> Instr s (t : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (t1 : s) (t : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ ('TOption a : s)) =>
Instr inp out
SOME
    PartlyPushableStorage Value heavy
val Instr (heavy : s) (t1 : s)
instr -> Value heavy
-> Instr (heavy : s) (t : s) -> PushableStorageSplit s t
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value heavy
val (Instr (heavy : s) (t : s) -> PushableStorageSplit s t)
-> Instr (heavy : s) (t : s) -> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ Instr (heavy : s) (t1 : s)
instr Instr (heavy : s) (t1 : s)
-> Instr (t1 : s) (t : s) -> Instr (heavy : s) (t : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (t1 : s) (t : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ ('TOption a : s)) =>
Instr inp out
SOME

  VList ([Value t1]
vals :: [Value tl]) -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope tl) of
    Right Dict (ConstantScope t1)
Dict -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
    Left BadTypeForScope
_     ->
      -- Here we check that even tho the type contains big_maps, we actually
      -- have big_maps in (one or more of) the values too.
      let handleList
            :: Instr s ('T.TList tl ': s) -> Value tl
            -> Maybe (Instr s ('T.TList tl ': s))
          handleList :: forall (s :: [T]).
Instr s ('TList t1 : s)
-> Value t1 -> Maybe (Instr s ('TList t1 : s))
handleList Instr s ('TList t1 : s)
instr Value t1
ele = case Value t1 -> PushableStorageSplit ('TList t1 : s) t1
forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage Value t1
ele of
            ConstantStorage Value t1
val ->
              Instr s ('TList t1 : s) -> Maybe (Instr s ('TList t1 : s))
forall a. a -> Maybe a
Just (Instr s ('TList t1 : s) -> Maybe (Instr s ('TList t1 : s)))
-> Instr s ('TList t1 : s) -> Maybe (Instr s ('TList t1 : s))
forall a b. (a -> b) -> a -> b
$ Instr s ('TList t1 : s)
instr Instr s ('TList t1 : s)
-> Instr ('TList t1 : s) (t1 : 'TList t1 : s)
-> Instr s (t1 : 'TList t1 : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Value t1 -> Instr ('TList t1 : s) (t1 : 'TList t1 : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value t1
val Instr s (t1 : 'TList t1 : s)
-> Instr (t1 : 'TList t1 : s) ('TList t1 : s)
-> Instr s ('TList t1 : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (t1 : 'TList t1 : s) ('TList t1 : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : 'TList a : s), out ~ ('TList a : s)) =>
Instr inp out
CONS
            PushableValueStorage Instr ('TList t1 : s) (t1 : 'TList t1 : s)
eleInstr ->
              Instr s ('TList t1 : s) -> Maybe (Instr s ('TList t1 : s))
forall a. a -> Maybe a
Just (Instr s ('TList t1 : s) -> Maybe (Instr s ('TList t1 : s)))
-> Instr s ('TList t1 : s) -> Maybe (Instr s ('TList t1 : s))
forall a b. (a -> b) -> a -> b
$ Instr s ('TList t1 : s)
instr Instr s ('TList t1 : s)
-> Instr ('TList t1 : s) (t1 : 'TList t1 : s)
-> Instr s (t1 : 'TList t1 : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr ('TList t1 : s) (t1 : 'TList t1 : s)
eleInstr Instr s (t1 : 'TList t1 : s)
-> Instr (t1 : 'TList t1 : s) ('TList t1 : s)
-> Instr s ('TList t1 : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (t1 : 'TList t1 : s) ('TList t1 : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : 'TList a : s), out ~ ('TList a : s)) =>
Instr inp out
CONS
            PartlyPushableStorage Value heavy
_ Instr (heavy : 'TList t1 : s) (t1 : 'TList t1 : s)
_ -> Maybe (Instr s ('TList t1 : s))
forall a. Maybe a
Nothing
      in  PushableStorageSplit s t
-> (Instr s (t : s) -> PushableStorageSplit s t)
-> Maybe (Instr s (t : s))
-> PushableStorageSplit s t
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Value t -> Instr (t : s) (t : s) -> PushableStorageSplit s t
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value t
v Instr (t : s) (t : s)
forall (inp :: [T]). Instr inp inp
Nop) Instr s (t : s) -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Maybe (Instr s (t : s)) -> PushableStorageSplit s t)
-> Maybe (Instr s (t : s)) -> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$
            (Instr s ('TList t1 : s)
 -> Value t1 -> Maybe (Instr s ('TList t1 : s)))
-> Instr s ('TList t1 : s)
-> [Value t1]
-> Maybe (Instr s ('TList t1 : s))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Instr s ('TList t1 : s)
-> Value t1 -> Maybe (Instr s ('TList t1 : s))
forall (s :: [T]).
Instr s ('TList t1 : s)
-> Value t1 -> Maybe (Instr s ('TList t1 : s))
handleList Instr s ('TList t1 : s)
forall {inp :: [T]} {out :: [T]} (p :: T) (s :: [T]).
(inp ~ s, out ~ ('TList p : s), SingI p) =>
Instr inp out
NIL [Value t1]
vals

  VSet{} -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v

  VPair (Value' Instr l
v1 :: Value t1, Value' Instr r
v2 :: Value t2) ->
    Value' Instr l
-> (SingI l => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value' Instr l
v1 ((SingI l => PushableStorageSplit s t) -> PushableStorageSplit s t)
-> (SingI l => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ Value' Instr r
-> (SingI r => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value' Instr r
v2 ((SingI r => PushableStorageSplit s t) -> PushableStorageSplit s t)
-> (SingI r => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$
      forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @StorageScope @'T.TPair @t1 @t2 (((StorageScope l, StorageScope r) => PushableStorageSplit s t)
 -> PushableStorageSplit s t)
-> ((StorageScope l, StorageScope r) => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$
        let handlePair
              :: PushableStorageSplit s t2
              -> PushableStorageSplit (t2 ': s) t1
              -> PushableStorageSplit s ('T.TPair t1 t2)
            handlePair :: forall (s :: [T]).
PushableStorageSplit s r
-> PushableStorageSplit (r : s) l
-> PushableStorageSplit s ('TPair l r)
handlePair PushableStorageSplit s r
psp2 PushableStorageSplit (r : s) l
psp1 = case (PushableStorageSplit s r
psp2, PushableStorageSplit (r : s) l
psp1) of
              -- at least one side is a constant
              (ConstantStorage Value' Instr r
_, ConstantStorage Value' Instr l
_) ->
                Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
              (ConstantStorage Value' Instr r
val2, PushableStorageSplit (r : s) l
_) ->
                PushableStorageSplit s r
-> PushableStorageSplit (r : s) l
-> PushableStorageSplit s ('TPair l r)
forall (s :: [T]).
PushableStorageSplit s r
-> PushableStorageSplit (r : s) l
-> PushableStorageSplit s ('TPair l r)
handlePair (Instr s (r : s) -> PushableStorageSplit s r
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr s (r : s) -> PushableStorageSplit s r)
-> Instr s (r : s) -> PushableStorageSplit s r
forall a b. (a -> b) -> a -> b
$ Value' Instr r -> Instr s (r : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value' Instr r
val2) PushableStorageSplit (r : s) l
psp1
              (PushableStorageSplit s r
_, ConstantStorage Value' Instr l
val1) ->
                PushableStorageSplit s r
-> PushableStorageSplit (r : s) l
-> PushableStorageSplit s ('TPair l r)
forall (s :: [T]).
PushableStorageSplit s r
-> PushableStorageSplit (r : s) l
-> PushableStorageSplit s ('TPair l r)
handlePair PushableStorageSplit s r
psp2 (Instr (r : s) (l : r : s) -> PushableStorageSplit (r : s) l
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr (r : s) (l : r : s) -> PushableStorageSplit (r : s) l)
-> Instr (r : s) (l : r : s) -> PushableStorageSplit (r : s) l
forall a b. (a -> b) -> a -> b
$ Value' Instr l -> Instr (r : s) (l : r : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value' Instr l
val1)
              -- at least one side is a constant or has no big_map values
              (PushableValueStorage Instr s (r : s)
instr2, PushableValueStorage Instr (r : s) (l : r : s)
instr1) ->
                Instr s ('TPair l r : s) -> PushableStorageSplit s ('TPair l r)
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr s ('TPair l r : s) -> PushableStorageSplit s ('TPair l r))
-> Instr s ('TPair l r : s) -> PushableStorageSplit s ('TPair l r)
forall a b. (a -> b) -> a -> b
$ Instr s (r : s)
instr2 Instr s (r : s) -> Instr (r : s) (l : r : s) -> Instr s (l : r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (r : s) (l : r : s)
instr1 Instr s (l : r : s)
-> Instr (l : r : s) ('TPair l r : s) -> Instr s ('TPair l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (l : r : s) ('TPair l r : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR
              (PushableValueStorage Instr s (r : s)
instr2, PartlyPushableStorage Value heavy
val1 Instr (heavy : r : s) (l : r : s)
instr1) ->
                Value heavy
-> Instr (heavy : s) ('TPair l r : s)
-> PushableStorageSplit s ('TPair l r)
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value heavy
val1 (Instr (heavy : s) ('TPair l r : s)
 -> PushableStorageSplit s ('TPair l r))
-> Instr (heavy : s) ('TPair l r : s)
-> PushableStorageSplit s ('TPair l r)
forall a b. (a -> b) -> a -> b
$ Instr s (r : s) -> Instr (heavy : s) (heavy : r : s)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr s (r : s)
instr2 Instr (heavy : s) (heavy : r : s)
-> Instr (heavy : r : s) (l : r : s)
-> Instr (heavy : s) (l : r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (heavy : r : s) (l : r : s)
instr1 Instr (heavy : s) (l : r : s)
-> Instr (l : r : s) ('TPair l r : s)
-> Instr (heavy : s) ('TPair l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (l : r : s) ('TPair l r : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR
              (PartlyPushableStorage Value heavy
val2 Instr (heavy : s) (r : s)
instr2, PushableValueStorage Instr (r : s) (l : r : s)
instr1) ->
                Value heavy
-> Instr (heavy : s) ('TPair l r : s)
-> PushableStorageSplit s ('TPair l r)
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value heavy
val2 (Instr (heavy : s) ('TPair l r : s)
 -> PushableStorageSplit s ('TPair l r))
-> Instr (heavy : s) ('TPair l r : s)
-> PushableStorageSplit s ('TPair l r)
forall a b. (a -> b) -> a -> b
$ Instr (heavy : s) (r : s)
instr2 Instr (heavy : s) (r : s)
-> Instr (r : s) (l : r : s) -> Instr (heavy : s) (l : r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (r : s) (l : r : s)
instr1 Instr (heavy : s) (l : r : s)
-> Instr (l : r : s) ('TPair l r : s)
-> Instr (heavy : s) ('TPair l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (l : r : s) ('TPair l r : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR
              -- both sides contain a big_map
              (PartlyPushableStorage Value heavy
val2 Instr (heavy : s) (r : s)
instr2, PartlyPushableStorage Value heavy
val1 Instr (heavy : r : s) (l : r : s)
instr1) ->
                Value ('TPair heavy heavy)
-> Instr ('TPair heavy heavy : s) ('TPair l r : s)
-> PushableStorageSplit s ('TPair l r)
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage ((Value heavy, Value heavy) -> Value ('TPair heavy heavy)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value heavy
val1, Value heavy
val2)) (Instr ('TPair heavy heavy : s) ('TPair l r : s)
 -> PushableStorageSplit s ('TPair l r))
-> Instr ('TPair heavy heavy : s) ('TPair l r : s)
-> PushableStorageSplit s ('TPair l r)
forall a b. (a -> b) -> a -> b
$
                  Instr ('TPair heavy heavy : s) (heavy : heavy : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : b : s)) =>
Instr inp out
UNPAIR Instr ('TPair heavy heavy : s) (heavy : heavy : s)
-> Instr (heavy : heavy : s) (heavy : r : s)
-> Instr ('TPair heavy heavy : s) (heavy : r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (heavy : s) (r : s)
-> Instr (heavy : heavy : s) (heavy : r : s)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr (heavy : s) (r : s)
instr2 Instr ('TPair heavy heavy : s) (heavy : r : s)
-> Instr (heavy : r : s) (l : r : s)
-> Instr ('TPair heavy heavy : s) (l : r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (heavy : r : s) (l : r : s)
instr1 Instr ('TPair heavy heavy : s) (l : r : s)
-> Instr (l : r : s) ('TPair l r : s)
-> Instr ('TPair heavy heavy : s) ('TPair l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (l : r : s) ('TPair l r : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR
        in PushableStorageSplit s r
-> PushableStorageSplit (r : s) l
-> PushableStorageSplit s ('TPair l r)
forall (s :: [T]).
PushableStorageSplit s r
-> PushableStorageSplit (r : s) l
-> PushableStorageSplit s ('TPair l r)
handlePair (Value' Instr r -> PushableStorageSplit s r
forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage Value' Instr r
v2) (Value' Instr l -> PushableStorageSplit (r : s) l
forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage Value' Instr l
v1)

  VOr (Left Value l
orVal :: Either (Value t1) (Value t2)) ->
    Value l
-> (SingI l => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value l
orVal ((SingI l => PushableStorageSplit s t) -> PushableStorageSplit s t)
-> (SingI l => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @StorageScope @'T.TOr @t1 @t2 (((StorageScope l, StorageScope r) => PushableStorageSplit s t)
 -> PushableStorageSplit s t)
-> ((StorageScope l, StorageScope r) => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$
      case Value l -> PushableStorageSplit s l
forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage Value l
orVal of
        ConstantStorage Value l
val -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope t2) of
          -- note: here we need to check for the opposite branch too
          Right Dict (ConstantScope r)
Dict -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
          Left BadTypeForScope
_ -> Instr s ('TOr l r : s) -> PushableStorageSplit s ('TOr l r)
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr s ('TOr l r : s) -> PushableStorageSplit s ('TOr l r))
-> Instr s ('TOr l r : s) -> PushableStorageSplit s ('TOr l r)
forall a b. (a -> b) -> a -> b
$ Value l -> Instr s (l : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value l
val Instr s (l : s)
-> Instr (l : s) ('TOr l r : s) -> Instr s ('TOr l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (l : s) ('TOr l r : s)
forall {inp :: [T]} {out :: [T]} (b :: T) (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ ('TOr a b : s), SingI b) =>
Instr inp out
LEFT
        PushableValueStorage Instr s (l : s)
instr -> Instr s ('TOr l r : s) -> PushableStorageSplit s ('TOr l r)
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr s ('TOr l r : s) -> PushableStorageSplit s ('TOr l r))
-> Instr s ('TOr l r : s) -> PushableStorageSplit s ('TOr l r)
forall a b. (a -> b) -> a -> b
$ Instr s (l : s)
instr Instr s (l : s)
-> Instr (l : s) ('TOr l r : s) -> Instr s ('TOr l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (l : s) ('TOr l r : s)
forall {inp :: [T]} {out :: [T]} (b :: T) (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ ('TOr a b : s), SingI b) =>
Instr inp out
LEFT
        PartlyPushableStorage Value heavy
val Instr (heavy : s) (l : s)
instr -> Value heavy
-> Instr (heavy : s) ('TOr l r : s)
-> PushableStorageSplit s ('TOr l r)
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value heavy
val (Instr (heavy : s) ('TOr l r : s)
 -> PushableStorageSplit s ('TOr l r))
-> Instr (heavy : s) ('TOr l r : s)
-> PushableStorageSplit s ('TOr l r)
forall a b. (a -> b) -> a -> b
$ Instr (heavy : s) (l : s)
instr Instr (heavy : s) (l : s)
-> Instr (l : s) ('TOr l r : s) -> Instr (heavy : s) ('TOr l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (l : s) ('TOr l r : s)
forall {inp :: [T]} {out :: [T]} (b :: T) (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ ('TOr a b : s), SingI b) =>
Instr inp out
LEFT
  VOr (Right Value r
orVal :: Either (Value t1) (Value t2)) ->
    Value r
-> (SingI r => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value r
orVal ((SingI r => PushableStorageSplit s t) -> PushableStorageSplit s t)
-> (SingI r => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @StorageScope @'T.TOr @t1 @t2 (((StorageScope l, StorageScope r) => PushableStorageSplit s t)
 -> PushableStorageSplit s t)
-> ((StorageScope l, StorageScope r) => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$
      case Value r -> PushableStorageSplit s r
forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage Value r
orVal of
        ConstantStorage Value r
val -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope t1) of
          -- note: here we need to check for the opposite branch too
          Right Dict (ConstantScope l)
Dict -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
          Left BadTypeForScope
_ -> Instr s ('TOr l r : s) -> PushableStorageSplit s ('TOr l r)
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr s ('TOr l r : s) -> PushableStorageSplit s ('TOr l r))
-> Instr s ('TOr l r : s) -> PushableStorageSplit s ('TOr l r)
forall a b. (a -> b) -> a -> b
$ Value r -> Instr s (r : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value r
val Instr s (r : s)
-> Instr (r : s) ('TOr l r : s) -> Instr s ('TOr l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (r : s) ('TOr l r : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (b : s), out ~ ('TOr a b : s), SingI a) =>
Instr inp out
RIGHT
        PushableValueStorage Instr s (r : s)
instr -> Instr s ('TOr l r : s) -> PushableStorageSplit s ('TOr l r)
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr s ('TOr l r : s) -> PushableStorageSplit s ('TOr l r))
-> Instr s ('TOr l r : s) -> PushableStorageSplit s ('TOr l r)
forall a b. (a -> b) -> a -> b
$ Instr s (r : s)
instr Instr s (r : s)
-> Instr (r : s) ('TOr l r : s) -> Instr s ('TOr l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (r : s) ('TOr l r : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (b : s), out ~ ('TOr a b : s), SingI a) =>
Instr inp out
RIGHT
        PartlyPushableStorage Value heavy
val Instr (heavy : s) (r : s)
instr -> Value heavy
-> Instr (heavy : s) ('TOr l r : s)
-> PushableStorageSplit s ('TOr l r)
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value heavy
val (Instr (heavy : s) ('TOr l r : s)
 -> PushableStorageSplit s ('TOr l r))
-> Instr (heavy : s) ('TOr l r : s)
-> PushableStorageSplit s ('TOr l r)
forall a b. (a -> b) -> a -> b
$ Instr (heavy : s) (r : s)
instr Instr (heavy : s) (r : s)
-> Instr (r : s) ('TOr l r : s) -> Instr (heavy : s) ('TOr l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (r : s) ('TOr l r : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (b : s), out ~ ('TOr a b : s), SingI a) =>
Instr inp out
RIGHT

  VMap (Map (Value k) (Value v)
vMap :: (Map (Value tk) (Value tv))) -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope tk) of
    Left BadTypeForScope
_ ->
      -- NOTE: all keys for a map need to be comparable and (even tho it's
      -- not a superclass) that means they have to be constants.
      -- I (@pasqu4le) found no exception to this rule, perhaps it should be
      -- enforced in the type system as well, but it may have more
      -- downsides than it's worth accepting.
      Text -> PushableStorageSplit s t
forall a. HasCallStack => Text -> a
error Text
"impossible: all map keys should be PUSHable"
    Right Dict (ConstantScope k)
Dict -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope tv) of
      Right Dict (ConstantScope v)
Dict -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
      Either BadTypeForScope (Dict (ConstantScope v))
_ -> forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @HasNoOp @'T.TMap @tk @tv (((HasNoOp k, HasNoOp v) => PushableStorageSplit s t)
 -> PushableStorageSplit s t)
-> ((HasNoOp k, HasNoOp v) => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$
        -- Similarly as for lists, here we check that even tho the value type
        -- contains a big_map, we actually have big_maps in (one or more of) them.
        let handleMap
              :: Instr s ('T.TMap tk tv ': s) -> (Value tk, Value tv)
              -> Maybe (Instr s ('T.TMap tk tv ': s))
            handleMap :: forall (s :: [T]).
Instr s ('TMap k v : s)
-> (Value k, Value v) -> Maybe (Instr s ('TMap k v : s))
handleMap Instr s ('TMap k v : s)
instr (Value k
key, Value v
ele) = case Value ('TOption v)
-> PushableStorageSplit ('TMap k v : s) ('TOption v)
forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage (Maybe (Value v) -> Value ('TOption v)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption (Maybe (Value v) -> Value ('TOption v))
-> Maybe (Value v) -> Value ('TOption v)
forall a b. (a -> b) -> a -> b
$ Value v -> Maybe (Value v)
forall a. a -> Maybe a
Just Value v
ele) of
              ConstantStorage Value ('TOption v)
val ->
                Instr s ('TMap k v : s) -> Maybe (Instr s ('TMap k v : s))
forall a. a -> Maybe a
Just (Instr s ('TMap k v : s) -> Maybe (Instr s ('TMap k v : s)))
-> Instr s ('TMap k v : s) -> Maybe (Instr s ('TMap k v : s))
forall a b. (a -> b) -> a -> b
$ Instr s ('TMap k v : s)
instr Instr s ('TMap k v : s)
-> Instr ('TMap k v : s) ('TOption v : 'TMap k v : s)
-> Instr s ('TOption v : 'TMap k v : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Value ('TOption v)
-> Instr ('TMap k v : s) ('TOption v : 'TMap k v : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value ('TOption v)
val Instr s ('TOption v : 'TMap k v : s)
-> Instr
     ('TOption v : 'TMap k v : s) (k : 'TOption v : 'TMap k v : s)
-> Instr s (k : 'TOption v : 'TMap k v : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Value k
-> Instr
     ('TOption v : 'TMap k v : s) (k : 'TOption v : 'TMap k v : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value k
key Instr s (k : 'TOption v : 'TMap k v : s)
-> Instr (k : 'TOption v : 'TMap k v : s) ('TMap k v : s)
-> Instr s ('TMap k v : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (k : 'TOption v : 'TMap k v : s) ('TMap k v : s)
forall {inp :: [T]} {out :: [T]} (c :: T) (s :: [T]).
(inp ~ (UpdOpKey c : UpdOpParams c : c : s), out ~ (c : s),
 UpdOp c) =>
Instr inp out
UPDATE
              PushableValueStorage Instr ('TMap k v : s) ('TOption v : 'TMap k v : s)
eleInstr ->
                Instr s ('TMap k v : s) -> Maybe (Instr s ('TMap k v : s))
forall a. a -> Maybe a
Just (Instr s ('TMap k v : s) -> Maybe (Instr s ('TMap k v : s)))
-> Instr s ('TMap k v : s) -> Maybe (Instr s ('TMap k v : s))
forall a b. (a -> b) -> a -> b
$ Instr s ('TMap k v : s)
instr Instr s ('TMap k v : s)
-> Instr ('TMap k v : s) ('TOption v : 'TMap k v : s)
-> Instr s ('TOption v : 'TMap k v : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr ('TMap k v : s) ('TOption v : 'TMap k v : s)
eleInstr Instr s ('TOption v : 'TMap k v : s)
-> Instr
     ('TOption v : 'TMap k v : s) (k : 'TOption v : 'TMap k v : s)
-> Instr s (k : 'TOption v : 'TMap k v : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Value k
-> Instr
     ('TOption v : 'TMap k v : s) (k : 'TOption v : 'TMap k v : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value k
key Instr s (k : 'TOption v : 'TMap k v : s)
-> Instr (k : 'TOption v : 'TMap k v : s) ('TMap k v : s)
-> Instr s ('TMap k v : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (k : 'TOption v : 'TMap k v : s) ('TMap k v : s)
forall {inp :: [T]} {out :: [T]} (c :: T) (s :: [T]).
(inp ~ (UpdOpKey c : UpdOpParams c : c : s), out ~ (c : s),
 UpdOp c) =>
Instr inp out
UPDATE
              PartlyPushableStorage Value heavy
_ Instr (heavy : 'TMap k v : s) ('TOption v : 'TMap k v : s)
_ -> Maybe (Instr s ('TMap k v : s))
forall a. Maybe a
Nothing
        in  PushableStorageSplit s t
-> (Instr s (t : s) -> PushableStorageSplit s t)
-> Maybe (Instr s (t : s))
-> PushableStorageSplit s t
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Value t -> Instr (t : s) (t : s) -> PushableStorageSplit s t
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value t
v Instr (t : s) (t : s)
forall (inp :: [T]). Instr inp inp
Nop) Instr s (t : s) -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Maybe (Instr s (t : s)) -> PushableStorageSplit s t)
-> Maybe (Instr s (t : s)) -> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$
              (Instr s ('TMap k v : s)
 -> (Value k, Value v) -> Maybe (Instr s ('TMap k v : s)))
-> Instr s ('TMap k v : s)
-> [(Value k, Value v)]
-> Maybe (Instr s ('TMap k v : s))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Instr s ('TMap k v : s)
-> (Value k, Value v) -> Maybe (Instr s ('TMap k v : s))
forall (s :: [T]).
Instr s ('TMap k v : s)
-> (Value k, Value v) -> Maybe (Instr s ('TMap k v : s))
handleMap Instr s ('TMap k v : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ s, out ~ ('TMap a b : s), SingI a, SingI b, Comparable a) =>
Instr inp out
EMPTY_MAP ([(Value k, Value v)] -> Maybe (Instr s ('TMap k v : s)))
-> [(Value k, Value v)] -> Maybe (Instr s ('TMap k v : s))
forall a b. (a -> b) -> a -> b
$ Map (Value k) (Value v) -> [(Value k, Value v)]
forall k a. Map k a -> [(k, a)]
M.toList Map (Value k) (Value v)
vMap

  VBigMap Maybe Natural
_ Map (Value' Instr k) (Value' Instr v)
_ -> Value t -> Instr (t : s) (t : s) -> PushableStorageSplit s t
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value t
v Instr (t : s) (t : s)
forall (inp :: [T]). Instr inp inp
Nop

-- | Whether this instruction is a real Michelson instruction.
--
-- Only the root is in question, children in the instruction tree are not
-- accounted for.
--
-- >>> isMichelsonInstr (Seq Nop Nop)
-- True
--
-- >>> isMichelsonInstr (Ext $ COMMENT_ITEM "comment")
-- False
--
-- This function is helpful e.g. in debugger.
isMichelsonInstr :: Instr i o -> Bool
isMichelsonInstr :: forall (i :: [T]) (o :: [T]). Instr i o -> Bool
isMichelsonInstr = \case
  WithLoc{} -> Bool
False
  Meta{} -> Bool
False
  FrameInstr{} -> Bool
False
  Seq{} -> Bool
True
  Instr i o
Nop -> Bool
False
  Ext{} -> Bool
False
  Nested{} -> Bool
True
  DocGroup{} -> Bool
False
  AnnCAR{} -> Bool
True
  AnnCDR{} -> Bool
True
  DROP{} -> Bool
True
  DROPN{} -> Bool
True
  AnnDUP{} -> Bool
True
  AnnDUPN{} -> Bool
True
  SWAP{} -> Bool
True
  DIG{} -> Bool
True
  DUG{} -> Bool
True
  AnnPUSH{} -> Bool
True
  AnnSOME{} -> Bool
True
  AnnNONE{} -> Bool
True
  AnnUNIT{} -> Bool
True
  IF_NONE{} -> Bool
True
  AnnPAIR{} -> Bool
True
  AnnUNPAIR{} -> Bool
True
  AnnPAIRN{} -> Bool
True
  UNPAIRN{} -> Bool
True
  AnnLEFT{} -> Bool
True
  AnnRIGHT{} -> Bool
True
  IF_LEFT{} -> Bool
True
  AnnNIL{} -> Bool
True
  AnnCONS{} -> Bool
True
  IF_CONS{} -> Bool
True
  AnnSIZE{} -> Bool
True
  AnnEMPTY_SET{} -> Bool
True
  AnnEMPTY_MAP{} -> Bool
True
  AnnEMPTY_BIG_MAP{} -> Bool
True
  AnnMAP{} -> Bool
True
  ITER{} -> Bool
True
  AnnMEM{} -> Bool
True
  AnnGET{} -> Bool
True
  AnnGETN{} -> Bool
True
  AnnUPDATE{} -> Bool
True
  AnnUPDATEN{} -> Bool
True
  AnnGET_AND_UPDATE{} -> Bool
True
  IF{} -> Bool
True
  LOOP{} -> Bool
True
  LOOP_LEFT{} -> Bool
True
  AnnLAMBDA{} -> Bool
True
  AnnEXEC{} -> Bool
True
  AnnAPPLY{} -> Bool
True
  DIP{} -> Bool
True
  DIPN{} -> Bool
True
  FAILWITH{} -> Bool
True
  AnnCAST{} -> Bool
True
  AnnRENAME{} -> Bool
True
  AnnPACK{} -> Bool
True
  AnnUNPACK{} -> Bool
True
  AnnCONCAT{} -> Bool
True
  AnnCONCAT'{} -> Bool
True
  AnnSLICE{} -> Bool
True
  AnnISNAT{} -> Bool
True
  AnnADD{} -> Bool
True
  AnnSUB{} -> Bool
True
  AnnSUB_MUTEZ{} -> Bool
True
  AnnMUL{} -> Bool
True
  AnnEDIV{} -> Bool
True
  AnnABS{} -> Bool
True
  AnnNEG{} -> Bool
True
  AnnLSL{} -> Bool
True
  AnnLSR{} -> Bool
True
  AnnOR{} -> Bool
True
  AnnAND{} -> Bool
True
  AnnXOR{} -> Bool
True
  AnnNOT{} -> Bool
True
  AnnCOMPARE{} -> Bool
True
  AnnEQ{} -> Bool
True
  AnnNEQ{} -> Bool
True
  AnnLT{} -> Bool
True
  AnnGT{} -> Bool
True
  AnnLE{} -> Bool
True
  AnnGE{} -> Bool
True
  AnnINT{} -> Bool
True
  AnnVIEW{} -> Bool
True
  AnnSELF{} -> Bool
True
  AnnCONTRACT{} -> Bool
True
  AnnTRANSFER_TOKENS{} -> Bool
True
  AnnSET_DELEGATE{} -> Bool
True
  AnnCREATE_CONTRACT{} -> Bool
True
  AnnIMPLICIT_ACCOUNT{} -> Bool
True
  AnnNOW{} -> Bool
True
  AnnAMOUNT{} -> Bool
True
  AnnBALANCE{} -> Bool
True
  AnnVOTING_POWER{} -> Bool
True
  AnnTOTAL_VOTING_POWER{} -> Bool
True
  AnnCHECK_SIGNATURE{} -> Bool
True
  AnnSHA256{} -> Bool
True
  AnnSHA512{} -> Bool
True
  AnnBLAKE2B{} -> Bool
True
  AnnSHA3{} -> Bool
True
  AnnKECCAK{} -> Bool
True
  AnnHASH_KEY{} -> Bool
True
  AnnPAIRING_CHECK{} -> Bool
True
  AnnSOURCE{} -> Bool
True
  AnnSENDER{} -> Bool
True
  AnnADDRESS{} -> Bool
True
  AnnCHAIN_ID{} -> Bool
True
  AnnLEVEL{} -> Bool
True
  AnnSELF_ADDRESS{} -> Bool
True
  NEVER{} -> Bool
True
  AnnTICKET{} -> Bool
True
  AnnREAD_TICKET{} -> Bool
True
  AnnSPLIT_TICKET{} -> Bool
True
  AnnJOIN_TICKETS{} -> Bool
True
  AnnOPEN_CHEST{} -> Bool
True
  AnnSAPLING_EMPTY_STATE{} -> Bool
True
  AnnSAPLING_VERIFY_UPDATE{} -> Bool
True
  AnnMIN_BLOCK_TIME{} -> Bool
True
  AnnEMIT{} -> Bool
True

-- | A wrapper around either typechecked 'Anns' or unchecked 'NonEmpty' of
-- 'AnyAnn'. Annotations on some instructions aren't typechecked, hence these
-- two constructors.
--
-- Helper for 'instrAnns'.
data SomeAnns where
  SomeAnns :: Anns xs -> SomeAnns
  SomeUncheckedAnns :: NonEmpty AnyAnn -> SomeAnns

-- | Get annotations from a typed 'Instr'. This doesn't recurse, use with
-- 'dfsFoldInstr' to collect all annotations in a tree/sequence.
instrAnns :: Instr i o -> Maybe SomeAnns
instrAnns :: forall (i :: [T]) (o :: [T]). Instr i o -> Maybe SomeAnns
instrAnns = \case
  WithLoc{} -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  Meta{} -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  FrameInstr{} -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  Seq{} -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  Instr i o
Nop -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  Ext{} -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  Nested{} -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  DocGroup{} -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  AnnCAR Anns '[VarAnn, FieldAnn]
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[VarAnn, FieldAnn] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[VarAnn, FieldAnn]
anns
  AnnCDR Anns '[VarAnn, FieldAnn]
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[VarAnn, FieldAnn] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[VarAnn, FieldAnn]
anns
  Instr i o
DROP -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  DROPN PeanoNatural n
_ -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  AnnDUP AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnDUPN AnnVar
anns PeanoNatural n
_ -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  Instr i o
SWAP -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  DIG PeanoNatural n
_ -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  DUG PeanoNatural n
_ -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  AnnPUSH Anns '[VarAnn, Notes t]
anns Value' Instr t
_ -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[VarAnn, Notes t] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[VarAnn, Notes t]
anns
  AnnSOME Anns '[TypeAnn, VarAnn]
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[TypeAnn, VarAnn] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[TypeAnn, VarAnn]
anns
  AnnNONE Anns '[TypeAnn, VarAnn, Notes a]
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[TypeAnn, VarAnn, Notes a] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[TypeAnn, VarAnn, Notes a]
anns
  AnnUNIT Anns '[TypeAnn, VarAnn]
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[TypeAnn, VarAnn] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[TypeAnn, VarAnn]
anns
  IF_NONE Instr s o
_ Instr (a : s) o
_ -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  AnnPAIR Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
anns
  AnnUNPAIR Anns '[VarAnn, VarAnn, FieldAnn, FieldAnn]
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[VarAnn, VarAnn, FieldAnn, FieldAnn] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[VarAnn, VarAnn, FieldAnn, FieldAnn]
anns
  AnnPAIRN AnnVar
anns PeanoNatural n
_ -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  UNPAIRN PeanoNatural n
_ -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  AnnLEFT Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes b]
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes b] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes b]
anns
  AnnRIGHT Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a]
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a]
anns
  IF_LEFT Instr (a : s) o
_ Instr (b : s) o
_ -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  AnnNIL Anns '[TypeAnn, VarAnn, Notes p]
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[TypeAnn, VarAnn, Notes p] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[TypeAnn, VarAnn, Notes p]
anns
  AnnCONS AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  IF_CONS Instr (a : 'TList a : s) o
_ Instr s o
_ -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  AnnSIZE AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnEMPTY_SET Anns '[TypeAnn, VarAnn, Notes e]
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[TypeAnn, VarAnn, Notes e] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[TypeAnn, VarAnn, Notes e]
anns
  AnnEMPTY_MAP Anns '[TypeAnn, VarAnn, Notes a, Notes b]
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[TypeAnn, VarAnn, Notes a, Notes b] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[TypeAnn, VarAnn, Notes a, Notes b]
anns
  AnnEMPTY_BIG_MAP Anns '[TypeAnn, VarAnn, Notes a, Notes b]
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[TypeAnn, VarAnn, Notes a, Notes b] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[TypeAnn, VarAnn, Notes a, Notes b]
anns
  AnnMAP AnnVar
anns Instr (MapOpInp c : s) (b : s)
_ -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  ITER Instr (IterOpEl c : o) o
_ -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  AnnMEM AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnGET AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnGETN AnnVar
anns PeanoNatural ix
_ -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnUPDATE AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnUPDATEN AnnVar
anns PeanoNatural ix
_ -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnGET_AND_UPDATE AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  IF Instr s o
_ Instr s o
_ -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  LOOP Instr o ('TBool : o)
_ -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  LOOP_LEFT Instr (a : s) ('TOr a b : s)
_ -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  AnnLAMBDA Anns '[VarAnn, Notes i, Notes o]
anns Value' Instr ('TLambda i o)
_ -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[VarAnn, Notes i, Notes o] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[VarAnn, Notes i, Notes o]
anns
  AnnEXEC AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnAPPLY AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  DIP Instr a c
_ -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  DIPN PeanoNatural n
_ Instr s s'
_ -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  Instr i o
FAILWITH -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  AnnCAST Anns '[VarAnn, Notes a]
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[VarAnn, Notes a] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[VarAnn, Notes a]
anns
  AnnRENAME AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnPACK AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnUNPACK Anns '[TypeAnn, VarAnn, Notes a]
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[TypeAnn, VarAnn, Notes a] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[TypeAnn, VarAnn, Notes a]
anns
  AnnCONCAT AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnCONCAT' AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnSLICE AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnISNAT AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnADD AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnSUB AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnSUB_MUTEZ AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnMUL AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnEDIV AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnABS AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnNEG AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnLSL AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnLSR AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnOR AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnAND AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnXOR AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnNOT AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnCOMPARE AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnEQ AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnNEQ AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnLT AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnGT AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnLE AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnGE AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnINT AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnVIEW Anns '[VarAnn, Notes ret]
anns ViewName
_ -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[VarAnn, Notes ret] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[VarAnn, Notes ret]
anns
  AnnSELF AnnVar
anns SomeEntrypointCallT arg
_ -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnCONTRACT Anns '[VarAnn, Notes p]
anns EpName
_ -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[VarAnn, Notes p] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[VarAnn, Notes p]
anns
  AnnTRANSFER_TOKENS AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnSET_DELEGATE AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnCREATE_CONTRACT Anns '[VarAnn, VarAnn]
anns Contract' Instr p g
_ -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ Anns '[VarAnn, VarAnn] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns Anns '[VarAnn, VarAnn]
anns
  AnnIMPLICIT_ACCOUNT AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnNOW AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnAMOUNT AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnBALANCE AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnVOTING_POWER AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnTOTAL_VOTING_POWER AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnCHECK_SIGNATURE AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnSHA256 AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnSHA512 AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnBLAKE2B AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnSHA3 AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnKECCAK AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnHASH_KEY AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnPAIRING_CHECK AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnSOURCE AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnSENDER AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnADDRESS AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnCHAIN_ID AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnLEVEL AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnSELF_ADDRESS AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  Instr i o
NEVER -> Maybe SomeAnns
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  AnnTICKET AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnREAD_TICKET AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnSPLIT_TICKET AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnJOIN_TICKETS AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnOPEN_CHEST AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnSAPLING_EMPTY_STATE AnnVar
anns Sing n
_ -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnSAPLING_VERIFY_UPDATE AnnVar
anns -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ AnnVar -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns AnnVar
anns
  AnnMIN_BLOCK_TIME [AnyAnn]
anns -> NonEmpty AnyAnn -> SomeAnns
SomeUncheckedAnns (NonEmpty AnyAnn -> SomeAnns)
-> Maybe (NonEmpty AnyAnn) -> Maybe SomeAnns
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [AnyAnn] -> Maybe (NonEmpty AnyAnn)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [AnyAnn]
anns
  AnnEMIT AnnVar
anns FieldAnn
tag Maybe (Notes t)
ty -> SomeAnns -> Maybe SomeAnns
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$
    case Maybe (Notes t)
ty of
      Just Notes t
ty' -> Anns '[FieldAnn, Notes t, VarAnn] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns (Anns '[FieldAnn, Notes t, VarAnn] -> SomeAnns)
-> Anns '[FieldAnn, Notes t, VarAnn] -> SomeAnns
forall a b. (a -> b) -> a -> b
$ FieldAnn
tag FieldAnn
-> Anns '[Notes t, VarAnn] -> Anns '[FieldAnn, Notes t, VarAnn]
forall {k} (tag :: k) (xs1 :: [*]).
Typeable tag =>
Annotation tag -> Anns xs1 -> Anns (Annotation tag : xs1)
`AnnsCons` Notes t
ty' Notes t -> AnnVar -> Anns '[Notes t, VarAnn]
forall (t :: T) (xs1 :: [*]).
SingI t =>
Notes t -> Anns xs1 -> Anns (Notes t : xs1)
`AnnsTyCons` AnnVar
anns
      Maybe (Notes t)
Nothing -> Anns '[FieldAnn, VarAnn] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns (Anns '[FieldAnn, VarAnn] -> SomeAnns)
-> Anns '[FieldAnn, VarAnn] -> SomeAnns
forall a b. (a -> b) -> a -> b
$ FieldAnn
tag FieldAnn -> AnnVar -> Anns '[FieldAnn, VarAnn]
forall {k} (tag :: k) (xs1 :: [*]).
Typeable tag =>
Annotation tag -> Anns xs1 -> Anns (Annotation tag : xs1)
`AnnsCons` AnnVar
anns