module Morley.Michelson.Typed.Util
( DfsSettings (..)
, CtorEffectsApp (..)
, ceaBottomToTop
, dfsInstr
, dfsFoldInstr
, dfsModifyInstr
, linearizeLeft
, linearizeLeftDeep
, dfsFoldMapValue
, dfsFoldMapValueM
, dfsMapValue
, dfsTraverseValue
, isStringValue
, isBytesValue
, allAtomicValues
, PushableStorageSplit (..)
, splitPushableStorage
) where
import Prelude hiding (Ordering(..))
import Control.Monad.Writer.Strict (execWriterT, runWriter, tell, writer)
import Data.Constraint (Dict(..))
import Data.Default (Default(..))
import qualified Data.Map as M
import qualified Data.Set as S
import GHC.Exts (fromList)
import qualified Text.Show
import Morley.Michelson.Text (MText)
import Morley.Michelson.Typed.Aliases
import Morley.Michelson.Typed.Contract
import Morley.Michelson.Typed.Instr
import Morley.Michelson.Typed.Scope
import qualified Morley.Michelson.Typed.T as T
import Morley.Michelson.Typed.Value
import Morley.Michelson.Typed.View
data DfsSettings x = DfsSettings
{ DfsSettings x -> Bool
dsGoToValues :: Bool
, DfsSettings x -> CtorEffectsApp x
dsCtorEffectsApp :: CtorEffectsApp x
} deriving stock (Int -> DfsSettings x -> ShowS
[DfsSettings x] -> ShowS
DfsSettings x -> String
(Int -> DfsSettings x -> ShowS)
-> (DfsSettings x -> String)
-> ([DfsSettings x] -> ShowS)
-> Show (DfsSettings x)
forall x. Int -> DfsSettings x -> ShowS
forall x. [DfsSettings x] -> ShowS
forall x. DfsSettings x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DfsSettings x] -> ShowS
$cshowList :: forall x. [DfsSettings x] -> ShowS
show :: DfsSettings x -> String
$cshow :: forall x. DfsSettings x -> String
showsPrec :: Int -> DfsSettings x -> ShowS
$cshowsPrec :: forall x. Int -> DfsSettings x -> ShowS
Show)
data CtorEffectsApp x = CtorEffectsApp
{ CtorEffectsApp x -> Text
ceaName :: Text
, CtorEffectsApp x
-> forall (i :: [T]) (o :: [T]).
Semigroup x =>
x -> x -> Instr i o -> (Instr i o, x)
ceaApplyEffects
:: forall i o. Semigroup x => x -> x -> Instr i o -> (Instr i o, x)
}
instance Show (CtorEffectsApp x) where
show :: CtorEffectsApp x -> String
show CtorEffectsApp{Text
forall (i :: [T]) (o :: [T]).
Semigroup x =>
x -> x -> Instr i o -> (Instr i o, x)
ceaApplyEffects :: forall (i :: [T]) (o :: [T]).
Semigroup x =>
x -> x -> Instr i o -> (Instr i o, x)
ceaName :: Text
ceaApplyEffects :: forall x.
CtorEffectsApp x
-> forall (i :: [T]) (o :: [T]).
Semigroup x =>
x -> x -> Instr i o -> (Instr i o, x)
ceaName :: forall x. CtorEffectsApp x -> Text
..} = Text -> String
forall b a. (Show a, IsString b) => a -> b
show Text
ceaName
ceaBottomToTop :: CtorEffectsApp x
ceaBottomToTop :: CtorEffectsApp x
ceaBottomToTop = CtorEffectsApp :: forall x.
Text
-> (forall (i :: [T]) (o :: [T]).
Semigroup x =>
x -> x -> Instr i o -> (Instr i o, x))
-> CtorEffectsApp x
CtorEffectsApp
{ ceaName :: Text
ceaName = Text
"Apply after"
, ceaApplyEffects :: forall (i :: [T]) (o :: [T]).
Semigroup x =>
x -> x -> Instr i o -> (Instr i o, x)
ceaApplyEffects =
\x
effBefore x
effAfter Instr i o
instr -> (Instr i o
instr, x
effBefore x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
effAfter)
}
instance Default (DfsSettings x) where
def :: DfsSettings x
def = DfsSettings :: forall x. Bool -> CtorEffectsApp x -> DfsSettings x
DfsSettings
{ dsGoToValues :: Bool
dsGoToValues = Bool
False
, dsCtorEffectsApp :: CtorEffectsApp x
dsCtorEffectsApp = CtorEffectsApp x
forall x. CtorEffectsApp x
ceaBottomToTop
}
dfsInstr ::
forall x inp out. Semigroup x
=> DfsSettings x
-> (forall i o. Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr :: DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr settings :: DfsSettings x
settings@DfsSettings{Bool
CtorEffectsApp x
dsCtorEffectsApp :: CtorEffectsApp x
dsGoToValues :: Bool
dsCtorEffectsApp :: forall x. DfsSettings x -> CtorEffectsApp x
dsGoToValues :: forall x. DfsSettings x -> Bool
..} forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step 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 -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]) (i1 :: [T]) (o1 :: [T]) (i2 :: [T])
(o2 :: [T]).
(Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> (Instr i o, x)
recursion2 Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
Seq Instr inp b
i1 Instr b out
i2
WithLoc InstrCallStack
loc Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (InstrCallStack -> Instr inp out -> Instr inp out
forall (a :: [T]) (b :: [T]).
InstrCallStack -> Instr a b -> Instr a b
WithLoc InstrCallStack
loc) Instr inp out
i1
Meta SomeMeta
meta Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (SomeMeta -> Instr inp out -> Instr inp out
forall (a :: [T]) (b :: [T]). SomeMeta -> Instr a b -> Instr a b
Meta SomeMeta
meta) Instr inp out
i1
InstrWithNotes Proxy s
p Rec Notes topElems
notes Instr inp (topElems ++ s)
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (Proxy s
-> Rec Notes topElems
-> Instr inp (topElems ++ s)
-> Instr inp (topElems ++ s)
forall (a :: [T]) (topElems :: [T]) (s :: [T]).
(RMap topElems, RecordToList topElems,
ReifyConstraint Show Notes topElems,
ReifyConstraint NFData Notes topElems, Each '[SingI] topElems) =>
Proxy s
-> Rec Notes topElems
-> Instr a (topElems ++ s)
-> Instr a (topElems ++ s)
InstrWithNotes Proxy s
p Rec Notes topElems
notes) Instr inp out
Instr inp (topElems ++ s)
i1
InstrWithVarNotes NonEmpty VarAnn
varNotes Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (NonEmpty VarAnn -> Instr inp out -> Instr inp out
forall (a :: [T]) (b :: [T]).
NonEmpty VarAnn -> Instr a b -> Instr a b
InstrWithVarNotes NonEmpty VarAnn
varNotes) Instr inp out
i1
InstrWithVarAnns VarAnns
varAnns Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (VarAnns -> Instr inp out -> Instr inp out
forall (a :: [T]) (b :: [T]). VarAnns -> Instr a b -> Instr a b
InstrWithVarAnns VarAnns
varAnns) Instr inp out
i1
FrameInstr Proxy s
p Instr a b
i1 -> (Instr a b -> Instr inp out) -> Instr a b -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
forall (a :: [T]) (b :: [T]) (s :: [T]).
(KnownList a, KnownList b) =>
Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
FrameInstr Proxy s
p) Instr a b
i1
Nested Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
Nested Instr inp out
i1
DocGroup DocGrouping
dg Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (DocGrouping -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
DocGrouping -> Instr inp out -> Instr inp out
DocGroup DocGrouping
dg) Instr inp out
i1
Fn Text
t StackFn
sfn Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (Text -> StackFn -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
Text -> StackFn -> Instr inp out -> Instr inp out
Fn Text
t StackFn
sfn) 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
-> (Instr ('TOption a : s) out, x)
forall (i :: [T]) (o :: [T]) (i1 :: [T]) (o1 :: [T]) (i2 :: [T])
(o2 :: [T]).
(Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> (Instr i o, x)
recursion2 Instr s out -> Instr (a : s) out -> Instr ('TOption a : s) out
forall (s :: [T]) (s' :: [T]) (a :: T).
Instr s s' -> Instr (a : s) s' -> Instr ('TOption a : s) s'
IF_NONE Instr s out
i1 Instr (a : s) out
i2
IF_LEFT 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
-> (Instr ('TOr a b : s) out, x)
forall (i :: [T]) (o :: [T]) (i1 :: [T]) (o1 :: [T]) (i2 :: [T])
(o2 :: [T]).
(Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> (Instr i o, x)
recursion2 Instr (a : s) out -> Instr (b : s) out -> Instr ('TOr a b : s) out
forall (a :: T) (s :: [T]) (s' :: [T]) (b :: T).
Instr (a : s) s' -> Instr (b : s) s' -> Instr ('TOr a b : s) s'
IF_LEFT Instr (a : s) out
i1 Instr (b : s) out
i2
IF_CONS 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
-> (Instr ('TList a : s) out, x)
forall (i :: [T]) (o :: [T]) (i1 :: [T]) (o1 :: [T]) (i2 :: [T])
(o2 :: [T]).
(Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> (Instr i o, x)
recursion2 Instr (a : 'TList a : s) out
-> Instr s out -> Instr ('TList a : s) out
forall (s :: T) (s :: [T]) (s' :: [T]).
Instr (s : 'TList s : s) s'
-> Instr s s' -> Instr ('TList s : s) s'
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 -> (Instr ('TBool : s) out, x)
forall (i :: [T]) (o :: [T]) (i1 :: [T]) (o1 :: [T]) (i2 :: [T])
(o2 :: [T]).
(Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> (Instr i o, x)
recursion2 Instr s out -> Instr s out -> Instr ('TBool : s) out
forall (s :: [T]) (s' :: [T]).
Instr s s' -> Instr s s' -> Instr ('TBool : s) s'
IF Instr s out
i1 Instr s out
i2
MAP Instr (MapOpInp c : s) (b : s)
i1 -> (Instr (MapOpInp c : s) (b : s) -> Instr (c : s) out)
-> Instr (MapOpInp c : s) (b : s) -> (Instr (c : s) out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 Instr (MapOpInp c : s) (b : s) -> Instr (c : s) out
forall (c :: T) (b :: T) (s :: [T]).
(MapOp c, SingI b) =>
Instr (MapOpInp c : s) (b : s) -> Instr (c : s) (MapOpRes c b : s)
MAP 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 -> (Instr (c : out) out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 Instr (IterOpEl c : out) out -> Instr (c : out) out
forall (c :: T) (s :: [T]).
IterOp c =>
Instr (IterOpEl c : s) s -> Instr (c : s) s
ITER Instr (IterOpEl c : out) out
i1
LOOP Instr out ('TBool : out)
i1 -> (Instr out ('TBool : out) -> Instr ('TBool : out) out)
-> Instr out ('TBool : out) -> (Instr ('TBool : out) out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 Instr out ('TBool : out) -> Instr ('TBool : out) out
forall (s :: [T]). Instr s ('TBool : s) -> Instr ('TBool : s) s
LOOP Instr out ('TBool : out)
i1
LOOP_LEFT Instr (a : s) ('TOr a b : s)
i1 -> (Instr (a : s) ('TOr a b : s) -> Instr ('TOr a b : s) (b : s))
-> Instr (a : s) ('TOr a b : s)
-> (Instr ('TOr a b : s) (b : s), x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 Instr (a : s) ('TOr a b : s) -> Instr ('TOr a b : s) (b : s)
forall (a :: T) (s :: [T]) (b :: T).
Instr (a : s) ('TOr a b : s) -> Instr ('TOr a b : s) (b : s)
LOOP_LEFT Instr (a : s) ('TOr a b : s)
i1
DIP Instr a c
i1 -> (Instr a c -> Instr (b : a) (b : c))
-> Instr a c -> (Instr (b : a) (b : c), x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 Instr a c -> Instr (b : a) (b : c)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr a c
i1
DIPN PeanoNatural n
s Instr s s'
i1 -> (Instr s s' -> Instr inp out) -> Instr s s' -> (Instr inp out, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (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
PUSH Value' Instr t
v -> (Instr inp out, x)
-> Maybe (Instr inp out, x) -> (Instr inp out, x)
forall a. a -> Maybe a -> a
fromMaybe (Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i) do
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
dsGoToValues
let
valueStep :: forall t . Value t -> (Value t, Maybe x)
valueStep :: Value t -> (Value t, Maybe x)
valueStep = \case
VLam RemFail Instr '[inp] '[out]
lambda -> (Instr '[inp] '[out] -> Value' Instr ('TLambda inp out))
-> (x -> Maybe x)
-> (Instr '[inp] '[out], x)
-> (Value' Instr ('TLambda inp out), Maybe x)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (RemFail Instr '[inp] '[out] -> Value' Instr ('TLambda inp out)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(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) x -> Maybe x
forall a. a -> Maybe a
Just ((Instr '[inp] '[out], x)
-> (Value' Instr ('TLambda inp out), Maybe x))
-> (Instr '[inp] '[out], x)
-> (Value' Instr ('TLambda inp out), Maybe x)
forall a b. (a -> b) -> a -> b
$
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr '[inp] '[out]
-> (Instr '[inp] '[out], x)
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings x
settings forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step (RemFail Instr '[inp] '[out] -> Instr '[inp] '[out]
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
RemFail instr i o -> instr i o
rfAnyInstr RemFail Instr '[inp] '[out]
lambda)
Value t
otherV -> (Value t
otherV, Maybe x
forall a. Maybe a
Nothing)
let
(Value' Instr t
innerV, Maybe x
innerXMaybe) = Writer (Maybe x) (Value' Instr t) -> (Value' Instr t, Maybe x)
forall w a. Writer w a -> (a, w)
runWriter (Writer (Maybe x) (Value' Instr t) -> (Value' Instr t, Maybe x))
-> Writer (Maybe x) (Value' Instr t) -> (Value' Instr t, Maybe x)
forall a b. (a -> b) -> a -> b
$ (forall (t' :: T).
Value t' -> WriterT (Maybe x) Identity (Value t'))
-> Value' Instr t -> Writer (Maybe x) (Value' Instr t)
forall (t :: T) (m :: * -> *).
Monad m =>
(forall (t' :: T). Value t' -> m (Value t'))
-> Value t -> m (Value t)
dfsTraverseValue ((Value t', Maybe x) -> WriterT (Maybe x) Identity (Value t')
forall w (m :: * -> *) a. MonadWriter w m => (a, w) -> m a
writer ((Value t', Maybe x) -> WriterT (Maybe x) Identity (Value t'))
-> (Value t' -> (Value t', Maybe x))
-> Value t'
-> WriterT (Maybe x) Identity (Value t')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value t' -> (Value t', Maybe x)
forall (t :: T). Value t -> (Value t, Maybe x)
valueStep) Value' Instr t
v
x
innerX <- Maybe x
innerXMaybe
let (Instr inp (t : inp)
outerI, x
outerX) = Instr inp (t : inp) -> (Instr inp (t : inp), x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step (Instr inp (t : inp) -> (Instr inp (t : inp), x))
-> Instr inp (t : inp) -> (Instr inp (t : inp), x)
forall a b. (a -> b) -> a -> b
$ Value' Instr t -> Instr inp (t : inp)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr t
innerV
pure $ CtorEffectsApp x
-> x -> x -> Instr inp (t : inp) -> (Instr inp (t : inp), x)
forall x.
CtorEffectsApp x
-> forall (i :: [T]) (o :: [T]).
Semigroup x =>
x -> x -> Instr i o -> (Instr i o, x)
ceaApplyEffects CtorEffectsApp x
dsCtorEffectsApp x
innerX x
outerX Instr inp (t : inp)
outerI
LAMBDA (VLam RemFail Instr '[inp] '[out]
i1)
| Bool
dsGoToValues ->
(Instr '[inp] '[out] -> Instr inp ('TLambda inp out : inp))
-> Instr '[inp] '[out] -> (Instr inp ('TLambda inp out : inp), x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (Value' Instr ('TLambda inp out)
-> Instr inp ('TLambda inp out : inp)
forall (i :: T) (o :: T) (s :: [T]).
(SingI i, SingI o) =>
Value' Instr ('TLambda i o) -> Instr s ('TLambda i o : s)
LAMBDA (Value' Instr ('TLambda inp out)
-> Instr inp ('TLambda inp out : inp))
-> (Instr '[inp] '[out] -> Value' Instr ('TLambda inp out))
-> Instr '[inp] '[out]
-> Instr inp ('TLambda inp out : inp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RemFail Instr '[inp] '[out] -> Value' Instr ('TLambda inp out)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(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) (RemFail Instr '[inp] '[out] -> Instr '[inp] '[out]
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
RemFail instr i o -> instr i o
rfAnyInstr RemFail Instr '[inp] '[out]
i1)
| Bool
otherwise -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
CREATE_CONTRACT Contract' Instr p g
contract
| Bool
dsGoToValues ->
let
(Instr (ContractInp p g) (ContractOut g)
codeI, x
codeX) = DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr (ContractInp p g) (ContractOut g)
-> (Instr (ContractInp p g) (ContractOut g), x)
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings x
settings forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step (Contract' Instr p g -> Instr (ContractInp p g) (ContractOut g)
forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> ContractCode' instr cp st
cCode Contract' Instr p g
contract)
([SomeView' Instr g]
viewsI, [x]
viewsX) = [(SomeView' Instr g, x)] -> ([SomeView' Instr g], [x])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(SomeView' Instr g, x)] -> ([SomeView' Instr g], [x]))
-> [(SomeView' Instr g, x)] -> ([SomeView' Instr g], [x])
forall a b. (a -> b) -> a -> b
$ ViewsSet' Instr g -> [Element (ViewsSet' Instr g)]
forall t. Container t => t -> [Element t]
toList (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' Instr g]
-> (SomeView' Instr g -> (SomeView' Instr g, x))
-> [(SomeView' Instr g, x)]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(SomeView View' Instr arg g ret
v) ->
(ViewCode' Instr arg g ret -> SomeView' Instr g)
-> (ViewCode' Instr arg g ret, x) -> (SomeView' Instr g, x)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (\ViewCode' Instr arg g ret
c -> 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 :: ViewCode' Instr arg g ret
vCode = ViewCode' Instr arg g ret
c }) ((ViewCode' Instr arg g ret, x) -> (SomeView' Instr g, x))
-> (ViewCode' Instr arg g ret, x) -> (SomeView' Instr g, x)
forall a b. (a -> b) -> a -> b
$ DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> ViewCode' Instr arg g ret
-> (ViewCode' Instr arg g ret, x)
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings x
settings forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step (ViewCode' Instr arg g ret -> (ViewCode' Instr arg g ret, x))
-> ViewCode' Instr arg g ret -> (ViewCode' Instr arg g ret, x)
forall a b. (a -> b) -> a -> b
$ View' Instr arg g ret -> ViewCode' Instr 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
(Instr
('TOption 'TKeyHash : 'TMutez : g : s)
('TOperation : 'TAddress : s)
i', x
x) = Instr
('TOption 'TKeyHash : 'TMutez : g : s)
('TOperation : 'TAddress : s)
-> (Instr
('TOption 'TKeyHash : 'TMutez : g : s)
('TOperation : 'TAddress : s),
x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step (Instr
('TOption 'TKeyHash : 'TMutez : g : s)
('TOperation : 'TAddress : s)
-> (Instr
('TOption 'TKeyHash : 'TMutez : g : s)
('TOperation : 'TAddress : s),
x))
-> Instr
('TOption 'TKeyHash : 'TMutez : g : s)
('TOperation : 'TAddress : s)
-> (Instr
('TOption 'TKeyHash : 'TMutez : g : s)
('TOperation : 'TAddress : s),
x)
forall a b. (a -> b) -> a -> b
$ Contract' Instr p g
-> Instr
('TOption 'TKeyHash : 'TMutez : g : s)
('TOperation : 'TAddress : s)
forall (p :: T) (g :: T) (s :: [T]).
(ParameterScope p, StorageScope g) =>
Contract' Instr p g
-> Instr
('TOption 'TKeyHash : 'TMutez : g : s)
('TOperation : 'TAddress : s)
CREATE_CONTRACT (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 :: Instr (ContractInp p g) (ContractOut g)
cCode = 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
$ [Item (Seq $ SomeView' Instr g)] -> Seq $ SomeView' Instr g
forall l. IsList l => [Item l] -> l
fromList [Item (Seq $ SomeView' Instr g)]
[SomeView' Instr g]
viewsI
}
in CtorEffectsApp x
-> x
-> x
-> Instr
('TOption 'TKeyHash : 'TMutez : g : s)
('TOperation : 'TAddress : s)
-> (Instr
('TOption 'TKeyHash : 'TMutez : g : s)
('TOperation : 'TAddress : s),
x)
forall x.
CtorEffectsApp x
-> forall (i :: [T]) (o :: [T]).
Semigroup x =>
x -> x -> Instr i o -> (Instr i o, x)
ceaApplyEffects CtorEffectsApp x
dsCtorEffectsApp (NonEmpty x -> x
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty x -> x) -> NonEmpty x -> x
forall a b. (a -> b) -> a -> b
$ x
codeX x -> [x] -> NonEmpty x
forall a. a -> [a] -> NonEmpty a
:| [x]
viewsX) x
x Instr
('TOption 'TKeyHash : 'TMutez : g : s)
('TOperation : 'TAddress : s)
i'
| Bool
otherwise -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
Nop{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
Ext (TEST_ASSERT (TestAssert Text
nm PrintComment inp
pc Instr inp ('TBool : out)
i1)) ->
(Instr inp ('TBool : out) -> Instr inp inp)
-> Instr inp ('TBool : out) -> (Instr inp inp, x)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 (ExtInstr inp -> Instr inp inp
forall (s :: [T]). ExtInstr s -> Instr s s
Ext (ExtInstr inp -> Instr inp inp)
-> (Instr inp ('TBool : out) -> ExtInstr inp)
-> Instr inp ('TBool : out)
-> Instr inp inp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestAssert inp -> ExtInstr inp
forall (s :: [T]). TestAssert s -> ExtInstr s
TEST_ASSERT (TestAssert inp -> ExtInstr inp)
-> (Instr inp ('TBool : out) -> TestAssert inp)
-> Instr inp ('TBool : out)
-> ExtInstr inp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text
-> PrintComment inp -> Instr inp ('TBool : out) -> TestAssert inp
forall (inp :: [T]) (out :: [T]).
Text
-> PrintComment inp -> Instr inp ('TBool : out) -> TestAssert inp
TestAssert Text
nm PrintComment inp
pc) Instr inp ('TBool : out)
i1
Ext{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
AnnCAR{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
AnnCDR{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
DROP{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
DROPN{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
DUP{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
DUPN{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
SWAP{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
DIG{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
DUG{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
SOME{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
NONE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
UNIT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
AnnPAIR{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
AnnUNPAIR{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
PAIRN{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
UNPAIRN{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
AnnLEFT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
AnnRIGHT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
NIL{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
CONS{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
SIZE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
EMPTY_SET{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
EMPTY_MAP{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
EMPTY_BIG_MAP{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
MEM{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
GET{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
GETN{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
UPDATE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
UPDATEN{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
GET_AND_UPDATE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
EXEC{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
APPLY{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
FAILWITH{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
CAST{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
RENAME{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
PACK{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
UNPACK{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
CONCAT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
CONCAT'{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
SLICE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
ISNAT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
ADD{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
SUB{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
MUL{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
EDIV{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
ABS{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
NEG{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
LSL{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
LSR{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
OR{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
AND{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
XOR{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
NOT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
COMPARE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
EQ{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
NEQ{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
LT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
GT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
LE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
GE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
INT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
VIEW{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
SELF{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
CONTRACT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
TRANSFER_TOKENS{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
SET_DELEGATE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
IMPLICIT_ACCOUNT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
NOW{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
AMOUNT{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
BALANCE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
VOTING_POWER{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
TOTAL_VOTING_POWER{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
CHECK_SIGNATURE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
SHA256{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
SHA512{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
BLAKE2B{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
SHA3{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
KECCAK{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
HASH_KEY{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
PAIRING_CHECK{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
SOURCE{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
SENDER{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
ADDRESS{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
CHAIN_ID{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
LEVEL{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
SELF_ADDRESS{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
NEVER{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
TICKET{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
READ_TICKET{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
SPLIT_TICKET{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
JOIN_TICKETS{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
OPEN_CHEST{} -> Instr inp out -> (Instr inp out, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr inp out
i
where
recursion1 ::
forall a b c d. (Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 :: (Instr a b -> Instr c d) -> Instr a b -> (Instr c d, x)
recursion1 Instr a b -> Instr c d
constructor Instr a b
i0 =
let
(Instr a b
innerI, x
innerX) = DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr a b
-> (Instr a b, x)
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings x
settings forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr a b
i0
(Instr c d
outerI, x
outerX) = Instr c d -> (Instr c d, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step (Instr c d -> (Instr c d, x)) -> Instr c d -> (Instr c d, x)
forall a b. (a -> b) -> a -> b
$ Instr a b -> Instr c d
constructor Instr a b
innerI
in CtorEffectsApp x -> x -> x -> Instr c d -> (Instr c d, x)
forall x.
CtorEffectsApp x
-> forall (i :: [T]) (o :: [T]).
Semigroup x =>
x -> x -> Instr i o -> (Instr i o, x)
ceaApplyEffects CtorEffectsApp x
dsCtorEffectsApp x
innerX x
outerX Instr c d
outerI
recursion2 ::
forall i o i1 o1 i2 o2.
(Instr i1 o1 -> Instr i2 o2 -> Instr i o) ->
Instr i1 o1 -> Instr i2 o2 -> (Instr i o, x)
recursion2 :: (Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> (Instr i o, x)
recursion2 Instr i1 o1 -> Instr i2 o2 -> Instr i o
constructor Instr i1 o1
i1 Instr i2 o2
i2 =
let
(Instr i1 o1
i1', x
x1) = DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr i1 o1
-> (Instr i1 o1, x)
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings x
settings forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr i1 o1
i1
(Instr i2 o2
i2', x
x2) = DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr i2 o2
-> (Instr i2 o2, x)
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings x
settings forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step Instr i2 o2
i2
(Instr i o
i', x
x) = Instr i o -> (Instr i o, x)
forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x)
step (Instr i o -> (Instr i o, x)) -> Instr i o -> (Instr i o, x)
forall a b. (a -> b) -> a -> b
$ Instr i1 o1 -> Instr i2 o2 -> Instr i o
constructor Instr i1 o1
i1' Instr i2 o2
i2'
in CtorEffectsApp x -> x -> x -> Instr i o -> (Instr i o, x)
forall x.
CtorEffectsApp x
-> forall (i :: [T]) (o :: [T]).
Semigroup x =>
x -> x -> Instr i o -> (Instr i o, x)
ceaApplyEffects CtorEffectsApp x
dsCtorEffectsApp (x
x1 x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
x2) x
x Instr i o
i'
dfsFoldInstr
:: forall x inp out.
(Semigroup x)
=> DfsSettings x
-> (forall i o. Instr i o -> x)
-> Instr inp out
-> x
dfsFoldInstr :: DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> x)
-> Instr inp out
-> x
dfsFoldInstr DfsSettings x
settings forall (i :: [T]) (o :: [T]). Instr i o -> x
step Instr inp out
instr =
(Instr inp out, x) -> x
forall a b. (a, b) -> b
snd ((Instr inp out, x) -> x) -> (Instr inp out, x) -> x
forall a b. (a -> b) -> a -> b
$ DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings x
settings (\Instr i o
i -> (Instr i o
i, Instr i o -> x
forall (i :: [T]) (o :: [T]). Instr i o -> x
step Instr i o
i)) Instr inp out
instr
dfsModifyInstr
:: DfsSettings ()
-> (forall i o. Instr i o -> Instr i o)
-> Instr inp out
-> Instr inp out
dfsModifyInstr :: DfsSettings ()
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
dfsModifyInstr DfsSettings ()
settings forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
step Instr inp out
instr =
(Instr inp out, ()) -> Instr inp out
forall a b. (a, b) -> a
fst ((Instr inp out, ()) -> Instr inp out)
-> (Instr inp out, ()) -> Instr inp out
forall a b. (a -> b) -> a -> b
$ DfsSettings ()
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, ()))
-> Instr inp out
-> (Instr inp out, ())
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings ()
settings (\Instr i o
i -> (Instr i o -> Instr i o
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
step Instr i o
i, ())) Instr inp out
instr
analyzeInstrFailure :: HasCallStack => Instr i o -> RemFail Instr i o
analyzeInstrFailure :: Instr i o -> RemFail Instr i o
analyzeInstrFailure = Instr i o -> RemFail Instr i o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go
where
go :: Instr i o -> RemFail Instr i o
go :: Instr i o -> RemFail Instr i o
go = \case
WithLoc InstrCallStack
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 (InstrCallStack -> Instr i o -> Instr i o
forall (a :: [T]) (b :: [T]).
InstrCallStack -> Instr a b -> Instr a b
WithLoc InstrCallStack
loc Instr i o
i0)
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 (a :: [T]) (b :: [T]). SomeMeta -> Instr a b -> Instr a b
Meta SomeMeta
meta Instr i o
i0)
RemFail Instr i o
r -> RemFail Instr i o
r
InstrWithNotes Proxy s
p Rec Notes topElems
pn Instr i (topElems ++ s)
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
Instr i (topElems ++ s)
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 (Proxy s
-> Rec Notes topElems
-> Instr i (topElems ++ s)
-> Instr i (topElems ++ s)
forall (a :: [T]) (topElems :: [T]) (s :: [T]).
(RMap topElems, RecordToList topElems,
ReifyConstraint Show Notes topElems,
ReifyConstraint NFData Notes topElems, Each '[SingI] topElems) =>
Proxy s
-> Rec Notes topElems
-> Instr a (topElems ++ s)
-> Instr a (topElems ++ s)
InstrWithNotes Proxy s
p Rec Notes topElems
pn Instr i o
Instr i (topElems ++ s)
i0)
RfAlwaysFails forall (o' :: [T]). Instr i o'
i0 ->
Text -> RemFail Instr i o
forall a. HasCallStack => Text -> a
error (Text -> RemFail Instr i o) -> Text -> RemFail Instr i o
forall a b. (a -> b) -> a -> b
$ Text
"InstrWithNotes wraps always-failing instruction: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Instr i Any -> Text
forall b a. (Show a, IsString b) => a -> b
show Instr i Any
forall (o' :: [T]). Instr i o'
i0
InstrWithVarNotes NonEmpty VarAnn
vn 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 (NonEmpty VarAnn -> Instr i o -> Instr i o
forall (a :: [T]) (b :: [T]).
NonEmpty VarAnn -> Instr a b -> Instr a b
InstrWithVarNotes NonEmpty VarAnn
vn Instr i o
i0)
RfAlwaysFails forall (o' :: [T]). Instr i o'
i0 ->
Text -> RemFail Instr i o
forall a. HasCallStack => Text -> a
error (Text -> RemFail Instr i o) -> Text -> RemFail Instr i o
forall a b. (a -> b) -> a -> b
$ Text
"InstrWithVarNotes wraps always-failing instruction: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Instr i Any -> Text
forall b a. (Show a, IsString b) => a -> b
show Instr i Any
forall (o' :: [T]). Instr i o'
i0
InstrWithVarAnns VarAnns
vn 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 (VarAnns -> Instr i o -> Instr i o
forall (a :: [T]) (b :: [T]). VarAnns -> Instr a b -> Instr a b
InstrWithVarAnns VarAnns
vn Instr i o
i0)
RfAlwaysFails forall (o' :: [T]). Instr i o'
i0 ->
Text -> RemFail Instr i o
forall a. HasCallStack => Text -> a
error (Text -> RemFail Instr i o) -> Text -> RemFail Instr i o
forall a b. (a -> b) -> a -> b
$ Text
"InstrWithVarAnns wraps always-failing instruction: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Instr i Any -> Text
forall b a. (Show a, IsString b) => a -> b
show Instr i Any
forall (o' :: [T]). Instr i o'
i0
FrameInstr 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
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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
Seq Instr i b
a (forall (o' :: [T]). Instr b o' -> Instr i o')
-> RemFail Instr b o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i1 :: k) (i2 :: k) (o :: k).
(forall (o' :: k). instr i1 o' -> instr i2 o')
-> RemFail instr i1 o -> RemFail instr i2 o
`rfMapAnyInstr` Instr b o -> RemFail Instr b o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr b o
b
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 (s :: [T]). Instr s s
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 (s :: [T]). ExtInstr s -> Instr s s
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
Fn Text
t StackFn
sfn Instr i o
i -> Text -> StackFn -> Instr i o' -> Instr i o'
forall (inp :: [T]) (out :: [T]).
Text -> StackFn -> Instr inp out -> Instr inp out
Fn Text
t StackFn
sfn (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]) (s' :: [T]) (a :: T).
Instr s s' -> Instr (a : s) s' -> Instr ('TOption a : s) s'
IF_NONE (Instr s o -> RemFail Instr s o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr s o
l) (Instr (a : s) o -> RemFail Instr (a : s) o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr (a : s) o
r)
IF_LEFT 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]) (s' :: [T]) (b :: T).
Instr (a : s) s' -> Instr (b : s) s' -> Instr ('TOr a b : s) s'
IF_LEFT (Instr (a : s) o -> RemFail Instr (a : s) o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr (a : s) o
l) (Instr (b : s) o -> RemFail Instr (b : s) o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr (b : s) o
r)
IF_CONS 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 (s :: T) (s :: [T]) (s' :: [T]).
Instr (s : 'TList s : s) s'
-> Instr s s' -> Instr ('TList s : s) s'
IF_CONS (Instr (a : 'TList a : s) o -> RemFail Instr (a : 'TList a : s) o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr (a : 'TList a : s) o
l) (Instr s o -> RemFail Instr s o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr s o
r)
IF 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]) (s' :: [T]).
Instr s s' -> Instr s s' -> Instr ('TBool : s) s'
IF (Instr s o -> RemFail Instr s o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr s o
l) (Instr s o -> RemFail Instr s o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr s o
r)
i :: Instr i o
i@MAP{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@ITER{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@LOOP{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@LOOP_LEFT{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@LAMBDA{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@DIP{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@DIPN{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@AnnCAR{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@AnnCDR{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@DROP{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@DROPN{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@DUP{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@DUPN{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@SWAP{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@DIG{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@DUG{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@PUSH{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@SOME{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@NONE{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@UNIT{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@AnnPAIR{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@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@PAIRN{} -> 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@NIL{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@CONS{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@SIZE{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@EMPTY_SET{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@EMPTY_MAP{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@EMPTY_BIG_MAP{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@MEM{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@GET{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@GETN{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@UPDATE{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@UPDATEN{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@GET_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@EXEC{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@APPLY{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
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]) (t :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : s) t
FAILWITH
i :: Instr i o
i@Instr i o
CAST -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
RENAME -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
PACK -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
UNPACK -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
CONCAT -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
CONCAT' -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
SLICE -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
ISNAT -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
ADD -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
SUB -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
MUL -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
EDIV -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
ABS -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
NEG -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
LSL -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
LSR -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
OR -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
AND -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
XOR -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
NOT -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
COMPARE -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
EQ -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
NEQ -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
LT -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
GT -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
LE -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
GE -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
INT -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@VIEW{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@SELF{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@CONTRACT{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
TRANSFER_TOKENS -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
SET_DELEGATE -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@CREATE_CONTRACT{} -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
IMPLICIT_ACCOUNT -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
NOW -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
AMOUNT -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
BALANCE -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
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@Instr i o
TOTAL_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@Instr i o
CHECK_SIGNATURE -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
SHA256 -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
SHA512 -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
BLAKE2B -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
SHA3 -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
KECCAK -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
HASH_KEY -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
PAIRING_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@Instr i o
SOURCE -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
SENDER -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
ADDRESS -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
CHAIN_ID -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
LEVEL -> Instr i o -> RemFail Instr i o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i
i :: Instr i o
i@Instr i o
SELF_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]) (t :: [T]). Instr ('TNever : s) t
NEVER
i :: Instr i o
i@Instr i o
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@Instr i o
READ_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@Instr i o
SPLIT_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@Instr i o
JOIN_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@Instr i o
OPEN_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
linearizeLeft :: Instr inp out -> Instr inp out
linearizeLeft :: Instr inp out -> Instr inp out
linearizeLeft = Bool -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
Bool -> Instr inp out -> Instr inp out
linearizeLeftHelper Bool
False
where
linearizeLeftHelper :: Bool -> Instr inp out -> Instr inp out
linearizeLeftHelper :: 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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
Seq (Bool -> Instr inp b -> Instr inp b
forall (inp :: [T]) (out :: [T]).
Bool -> Instr inp out -> Instr inp out
linearizeLeftHelper Bool
isLeftInstrAlreadyLinear (Instr inp b -> Instr b b -> Instr inp b
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
Seq Instr inp b
i1 Instr b b
i2)) Instr b out
i3
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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
Seq Instr inp b
i1 Instr b out
i2
| Instr b out
Nop <- Instr b out
i2 -> Instr inp b -> Instr inp b
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
linearizeLeft Instr inp b
i1
| Bool
otherwise -> Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
Seq (Instr inp b -> Instr inp b
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
linearizeLeft Instr inp b
i1) Instr b out
i2
Instr inp out
i -> Instr inp out
i
linearizeLeftDeep :: Instr inp out -> Instr inp out
linearizeLeftDeep :: Instr inp out -> Instr inp out
linearizeLeftDeep = DfsSettings ()
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
forall (inp :: [T]) (out :: [T]).
DfsSettings ()
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
dfsModifyInstr DfsSettings ()
forall a. Default a => a
def forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
linearizeLeft
dfsMapValue ::
forall t.
(forall t'. Value t' -> Value t')
-> Value t
-> Value t
dfsMapValue :: (forall (t' :: T). Value t' -> Value t') -> Value t -> Value t
dfsMapValue forall (t' :: T). Value t' -> Value t'
step 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
$ (forall (t' :: T). Value t' -> Identity (Value t'))
-> Value t -> Identity (Value t)
forall (t :: T) (m :: * -> *).
Monad m =>
(forall (t' :: T). Value t' -> m (Value t'))
-> Value t -> m (Value t)
dfsTraverseValue (Value t' -> Identity (Value t')
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value t' -> Identity (Value t'))
-> (Value t' -> Value t') -> Value t' -> Identity (Value t')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value t' -> Value t'
forall (t' :: T). Value t' -> Value t'
step) Value t
v
dfsTraverseValue ::
forall t m.
(Monad m)
=> (forall t'. Value t' -> m (Value t'))
-> Value t
-> m (Value t)
dfsTraverseValue :: (forall (t' :: T). Value t' -> m (Value t'))
-> Value t -> m (Value t)
dfsTraverseValue forall (t' :: T). Value t' -> m (Value t')
step Value t
i = case Value t
i of
VKey{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
Value t
VUnit -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VSignature{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VChainId{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VOp{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VContract{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VTicket{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VLam{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VInt{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VNat{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VString{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VBytes{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VMutez{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VBool{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VKeyHash{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VBls12381Fr{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VBls12381G1{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VBls12381G2{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VTimestamp{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VAddress{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VChestKey{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VChest{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
VOption Maybe (Value' Instr t)
mVal -> case Maybe (Value' Instr t)
mVal of
Maybe (Value' Instr t)
Nothing -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step Value t
i
Just Value' Instr t
val -> (Value' Instr t -> Value t) -> Value' Instr t -> m (Value t)
forall (t' :: T). (Value t' -> Value t) -> Value t' -> m (Value t)
recursion1 (Maybe (Value' Instr t) -> Value' Instr ('TOption t)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value' Instr t) -> Value' Instr ('TOption t))
-> (Value' Instr t -> Maybe (Value' Instr t))
-> Value' Instr t
-> Value' Instr ('TOption t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' Instr t -> Maybe (Value' Instr t)
forall a. a -> Maybe a
Just) Value' Instr t
val
VList [Value' Instr t]
vals -> do
[Value' Instr t]
vs <- (Value' Instr t -> m (Value' Instr t))
-> [Value' Instr t] -> m [Value' Instr t]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((forall (t' :: T). Value t' -> m (Value t'))
-> Value' Instr t -> m (Value' Instr t)
forall (t :: T) (m :: * -> *).
Monad m =>
(forall (t' :: T). Value t' -> m (Value t'))
-> Value t -> m (Value t)
dfsTraverseValue forall (t' :: T). Value t' -> m (Value t')
step) [Value' Instr t]
vals
Value ('TList t) -> m (Value ('TList t))
forall (t' :: T). Value t' -> m (Value t')
step (Value ('TList t) -> m (Value ('TList t)))
-> Value ('TList t) -> m (Value ('TList t))
forall a b. (a -> b) -> a -> b
$ [Value' Instr t] -> Value ('TList t)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
[Value' instr t] -> Value' instr ('TList t)
VList [Value' Instr t]
vs
VSet Set (Value' Instr t)
vals -> do
Set (Value' Instr t)
cs <- [Value' Instr t] -> Set (Value' Instr t)
forall a. Ord a => [a] -> Set a
S.fromList ([Value' Instr t] -> Set (Value' Instr t))
-> m [Value' Instr t] -> m (Set (Value' Instr t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value' Instr t -> m (Value' Instr t))
-> [Value' Instr t] -> m [Value' Instr t]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((forall (t' :: T). Value t' -> m (Value t'))
-> Value' Instr t -> m (Value' Instr t)
forall (t :: T) (m :: * -> *).
Monad m =>
(forall (t' :: T). Value t' -> m (Value t'))
-> Value t -> m (Value t)
dfsTraverseValue forall (t' :: T). Value t' -> m (Value t')
step) (Set (Value' Instr t) -> [Value' Instr t]
forall a. Set a -> [a]
S.toList Set (Value' Instr t)
vals)
Value ('TSet t) -> m (Value ('TSet t))
forall (t' :: T). Value t' -> m (Value t')
step (Set (Value' Instr t) -> Value ('TSet t)
forall (t :: T) (instr :: [T] -> [T] -> *).
(SingI t, Comparable t) =>
Set (Value' instr t) -> Value' instr ('TSet t)
VSet Set (Value' Instr t)
cs)
VPair (Value' Instr l
v1, Value' Instr r
v2) -> do
Value' Instr l
v1' <- (forall (t' :: T). Value t' -> m (Value t'))
-> Value' Instr l -> m (Value' Instr l)
forall (t :: T) (m :: * -> *).
Monad m =>
(forall (t' :: T). Value t' -> m (Value t'))
-> Value t -> m (Value t)
dfsTraverseValue forall (t' :: T). Value t' -> m (Value t')
step Value' Instr l
v1
Value' Instr r
v2' <- (forall (t' :: T). Value t' -> m (Value t'))
-> Value' Instr r -> m (Value' Instr r)
forall (t :: T) (m :: * -> *).
Monad m =>
(forall (t' :: T). Value t' -> m (Value t'))
-> Value t -> m (Value t)
dfsTraverseValue forall (t' :: T). Value t' -> m (Value t')
step Value' Instr r
v2
Value ('TPair l r) -> m (Value ('TPair l r))
forall (t' :: T). Value t' -> m (Value t')
step (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 :: (Value t' -> Value t) -> Value t' -> m (Value t)
recursion1 Value t' -> Value t
constructor Value t'
v = do
Value t'
v' <- (forall (t' :: T). Value t' -> m (Value t'))
-> Value t' -> m (Value t')
forall (t :: T) (m :: * -> *).
Monad m =>
(forall (t' :: T). Value t' -> m (Value t'))
-> Value t -> m (Value t)
dfsTraverseValue forall (t' :: T). Value t' -> m (Value t')
step Value t'
v
Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step (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 :: (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' <- (forall (t' :: T). Value t' -> m (Value t'))
-> Value k -> m (Value k)
forall (t :: T) (m :: * -> *).
Monad m =>
(forall (t' :: T). Value t' -> m (Value t'))
-> Value t -> m (Value t)
dfsTraverseValue forall (t' :: T). Value t' -> m (Value t')
step Value k
k
Value v
v' <- (forall (t' :: T). Value t' -> m (Value t'))
-> Value v -> m (Value v)
forall (t :: T) (m :: * -> *).
Monad m =>
(forall (t' :: T). Value t' -> m (Value t'))
-> Value t -> m (Value t)
dfsTraverseValue forall (t' :: T). Value t' -> m (Value t')
step Value v
v
pure (Value k
k', Value v
v')
Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
step (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'
dfsFoldMapValue ::
Monoid x =>
(forall t'. Value t' -> x)
-> Value t
-> x
dfsFoldMapValue :: (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
dfsFoldMapValueM
:: (Monoid x, Monad m)
=> (forall t'. Value t' -> m x)
-> Value t
-> m x
dfsFoldMapValueM :: (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
$
(forall (t' :: T). Value t' -> WriterT x m (Value t'))
-> Value t -> WriterT x m (Value t)
forall (t :: T) (m :: * -> *).
Monad m =>
(forall (t' :: T). Value t' -> m (Value t'))
-> Value t -> m (Value t)
dfsTraverseValue
(\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
isStringValue :: Value t -> Maybe MText
isStringValue :: 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
isBytesValue :: Value t -> Maybe ByteString
isBytesValue :: 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
allAtomicValues ::
forall t a. (forall t'. Value t' -> Maybe a) -> Value t -> [a]
allAtomicValues :: (forall (t' :: T). Value t' -> Maybe a) -> Value t -> [a]
allAtomicValues 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)
data PushableStorageSplit s st where
ConstantStorage
:: ConstantScope st
=> Value st
-> PushableStorageSplit s st
PushableValueStorage
:: StorageScope st
=> Instr s (st ': s)
-> PushableStorageSplit s st
PartlyPushableStorage
:: (StorageScope heavy, StorageScope st)
=> Value heavy -> Instr (heavy ': s) (st ': s)
-> PushableStorageSplit s st
splitPushableStorage :: StorageScope t => Value t -> PushableStorageSplit s t
splitPushableStorage :: Value t -> PushableStorageSplit s t
splitPushableStorage Value t
v = case Value t
v of
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
VTicket{} -> Value t -> Instr (t : s) (t : s) -> PushableStorageSplit s t
forall (heavy :: T) (st :: T) (s :: [T]).
(StorageScope heavy, StorageScope st) =>
Value heavy
-> Instr (heavy : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value t
v Instr (t : s) (t : s)
forall (s :: [T]). Instr s s
Nop
VOption (Maybe (Value t)
Nothing :: Maybe (Value tm)) -> case CheckScope (ConstantScope t) =>
Either BadTypeForScope (Dict (ConstantScope t))
forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope tm) of
Right Dict (ConstantScope t)
Dict -> Value ('TOption t) -> PushableStorageSplit s ('TOption t)
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage (Value ('TOption t) -> PushableStorageSplit s ('TOption t))
-> Value ('TOption t) -> PushableStorageSplit s ('TOption t)
forall a b. (a -> b) -> a -> b
$ Maybe (Value t) -> Value ('TOption t)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption Maybe (Value t)
forall a. Maybe a
Nothing
Left BadTypeForScope
_ -> Instr s ('TOption t : s) -> PushableStorageSplit s ('TOption t)
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr s ('TOption t : s) -> PushableStorageSplit s ('TOption t))
-> Instr s ('TOption t : s) -> PushableStorageSplit s ('TOption t)
forall a b. (a -> b) -> a -> b
$ Instr s ('TOption t : s)
forall (s :: T) (s :: [T]). SingI s => Instr s ('TOption s : s)
NONE
VOption (Just Value t
jVal :: Maybe (Value tm)) -> case Value t -> PushableStorageSplit s t
forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage Value t
jVal of
ConstantStorage Value t
_ -> Value ('TOption t) -> PushableStorageSplit s ('TOption t)
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage (Value ('TOption t) -> PushableStorageSplit s ('TOption t))
-> (Maybe (Value t) -> Value ('TOption t))
-> Maybe (Value t)
-> PushableStorageSplit s ('TOption t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Value t) -> Value ('TOption t)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value t) -> PushableStorageSplit s ('TOption t))
-> Maybe (Value t) -> PushableStorageSplit s ('TOption t)
forall a b. (a -> b) -> a -> b
$ Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just Value t
jVal
PushableValueStorage Instr s (t : s)
instr -> Instr s ('TOption t : s) -> PushableStorageSplit s ('TOption t)
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr s ('TOption t : s) -> PushableStorageSplit s ('TOption t))
-> Instr s ('TOption t : s) -> PushableStorageSplit s ('TOption t)
forall a b. (a -> b) -> a -> b
$ Instr s (t : s)
instr Instr s (t : s)
-> Instr (t : s) ('TOption t : s) -> Instr s ('TOption t : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (t : s) ('TOption t : s)
forall (a :: T) (s :: [T]). Instr (a : s) ('TOption a : s)
SOME
PartlyPushableStorage Value heavy
val Instr (heavy : s) (t : s)
instr -> Value heavy
-> Instr (heavy : s) ('TOption t : s)
-> PushableStorageSplit s ('TOption t)
forall (heavy :: T) (st :: T) (s :: [T]).
(StorageScope heavy, StorageScope st) =>
Value heavy
-> Instr (heavy : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value heavy
val (Instr (heavy : s) ('TOption t : s)
-> PushableStorageSplit s ('TOption t))
-> Instr (heavy : s) ('TOption t : s)
-> PushableStorageSplit s ('TOption t)
forall a b. (a -> b) -> a -> b
$ Instr (heavy : s) (t : s)
instr Instr (heavy : s) (t : s)
-> Instr (t : s) ('TOption t : s)
-> Instr (heavy : s) ('TOption t : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (t : s) ('TOption t : s)
forall (a :: T) (s :: [T]). Instr (a : s) ('TOption a : s)
SOME
VList ([Value t]
vals :: [Value tl]) -> case CheckScope (ConstantScope t) =>
Either BadTypeForScope (Dict (ConstantScope t))
forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope tl) of
Right Dict (ConstantScope t)
Dict -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
Left BadTypeForScope
_ ->
let handleList
:: Instr s ('T.TList tl ': s) -> Value tl
-> Maybe (Instr s ('T.TList tl ': s))
handleList :: Instr s ('TList t : s) -> Value t -> Maybe (Instr s ('TList t : s))
handleList Instr s ('TList t : s)
instr Value t
ele = case Value t -> PushableStorageSplit ('TList t : s) t
forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage Value t
ele of
ConstantStorage Value t
val ->
Instr s ('TList t : s) -> Maybe (Instr s ('TList t : s))
forall a. a -> Maybe a
Just (Instr s ('TList t : s) -> Maybe (Instr s ('TList t : s)))
-> Instr s ('TList t : s) -> Maybe (Instr s ('TList t : s))
forall a b. (a -> b) -> a -> b
$ Instr s ('TList t : s)
instr Instr s ('TList t : s)
-> Instr ('TList t : s) (t : 'TList t : s)
-> Instr s (t : 'TList t : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Value t -> Instr ('TList t : s) (t : 'TList t : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value t
val Instr s (t : 'TList t : s)
-> Instr (t : 'TList t : s) ('TList t : s)
-> Instr s ('TList t : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (t : 'TList t : s) ('TList t : s)
forall (a :: T) (s :: [T]). Instr (a : 'TList a : s) ('TList a : s)
CONS
PushableValueStorage Instr ('TList t : s) (t : 'TList t : s)
eleInstr ->
Instr s ('TList t : s) -> Maybe (Instr s ('TList t : s))
forall a. a -> Maybe a
Just (Instr s ('TList t : s) -> Maybe (Instr s ('TList t : s)))
-> Instr s ('TList t : s) -> Maybe (Instr s ('TList t : s))
forall a b. (a -> b) -> a -> b
$ Instr s ('TList t : s)
instr Instr s ('TList t : s)
-> Instr ('TList t : s) (t : 'TList t : s)
-> Instr s (t : 'TList t : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr ('TList t : s) (t : 'TList t : s)
eleInstr Instr s (t : 'TList t : s)
-> Instr (t : 'TList t : s) ('TList t : s)
-> Instr s ('TList t : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (t : 'TList t : s) ('TList t : s)
forall (a :: T) (s :: [T]). Instr (a : 'TList a : s) ('TList a : s)
CONS
PartlyPushableStorage Value heavy
_ Instr (heavy : 'TList t : s) (t : 'TList t : s)
_ -> Maybe (Instr s ('TList t : 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 (heavy :: T) (st :: T) (s :: [T]).
(StorageScope heavy, StorageScope st) =>
Value heavy
-> Instr (heavy : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value t
v Instr (t : s) (t : s)
forall (s :: [T]). Instr s s
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 t : s)
-> Value t -> Maybe (Instr s ('TList t : s)))
-> Instr s ('TList t : s)
-> [Value t]
-> Maybe (Instr s ('TList t : s))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Instr s ('TList t : s) -> Value t -> Maybe (Instr s ('TList t : s))
forall (s :: [T]).
Instr s ('TList t : s) -> Value t -> Maybe (Instr s ('TList t : s))
handleList Instr s ('TList t : s)
forall (p :: T) (s :: [T]). SingI p => Instr s ('TList p : s)
NIL [Value t]
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 ret.
(WithDeMorganScope StorageScope 'TPair l r,
StorageScope ('TPair l r)) =>
((StorageScope l, StorageScope r) => ret) -> ret
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 :: 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
(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 (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
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 (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr l
val1)
(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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (l : r : s) ('TPair l r : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ (a : b : s), o ~ ('TPair a b : s)) =>
Instr i o
PAIR
(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 (heavy :: T) (st :: T) (s :: [T]).
(StorageScope heavy, StorageScope st) =>
Value heavy
-> Instr (heavy : 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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (l : r : s) ('TPair l r : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ (a : b : s), o ~ ('TPair a b : s)) =>
Instr i o
PAIR
(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 (heavy :: T) (st :: T) (s :: [T]).
(StorageScope heavy, StorageScope st) =>
Value heavy
-> Instr (heavy : 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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (l : r : s) ('TPair l r : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ (a : b : s), o ~ ('TPair a b : s)) =>
Instr i o
PAIR
(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 (heavy :: T) (st :: T) (s :: [T]).
(StorageScope heavy, StorageScope st) =>
Value heavy
-> Instr (heavy : 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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : b : s)) =>
Instr i o
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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (l : r : s) ('TPair l r : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ (a : b : s), o ~ ('TPair a b : s)) =>
Instr i o
PAIR
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 ret.
(WithDeMorganScope StorageScope 'TOr l r,
StorageScope ('TOr l r)) =>
((StorageScope l, StorageScope r) => ret) -> ret
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 CheckScope (ConstantScope r) =>
Either BadTypeForScope (Dict (ConstantScope r))
forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope t2) of
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 (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value l
val Instr s (l : s)
-> Instr (l : s) ('TOr l r : s) -> Instr s ('TOr l r : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (l : s) ('TOr l r : s)
forall (i :: [T]) (o :: [T]) (b :: T) (a :: T) (s :: [T]).
(SingI b, i ~ (a : s), o ~ ('TOr a b : s)) =>
Instr i o
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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (l : s) ('TOr l r : s)
forall (i :: [T]) (o :: [T]) (b :: T) (a :: T) (s :: [T]).
(SingI b, i ~ (a : s), o ~ ('TOr a b : s)) =>
Instr i o
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 (heavy :: T) (st :: T) (s :: [T]).
(StorageScope heavy, StorageScope st) =>
Value heavy
-> Instr (heavy : 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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (l : s) ('TOr l r : s)
forall (i :: [T]) (o :: [T]) (b :: T) (a :: T) (s :: [T]).
(SingI b, i ~ (a : s), o ~ ('TOr a b : s)) =>
Instr i o
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 ret.
(WithDeMorganScope StorageScope 'TOr l r,
StorageScope ('TOr l r)) =>
((StorageScope l, StorageScope r) => ret) -> ret
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 CheckScope (ConstantScope l) =>
Either BadTypeForScope (Dict (ConstantScope l))
forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope t1) of
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 (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value r
val Instr s (r : s)
-> Instr (r : s) ('TOr l r : s) -> Instr s ('TOr l r : s)
forall (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (r : s) ('TOr l r : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(SingI a, i ~ (b : s), o ~ ('TOr a b : s)) =>
Instr i o
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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (r : s) ('TOr l r : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(SingI a, i ~ (b : s), o ~ ('TOr a b : s)) =>
Instr i o
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 (heavy :: T) (st :: T) (s :: [T]).
(StorageScope heavy, StorageScope st) =>
Value heavy
-> Instr (heavy : 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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (r : s) ('TOr l r : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(SingI a, i ~ (b : s), o ~ ('TOr a b : s)) =>
Instr i o
RIGHT
VMap (Map (Value k) (Value v)
vMap :: (Map (Value tk) (Value tv))) -> case CheckScope (ConstantScope k) =>
Either BadTypeForScope (Dict (ConstantScope k))
forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope tk) of
Left BadTypeForScope
_ ->
Text -> PushableStorageSplit s t
forall a. HasCallStack => Text -> a
error Text
"impossible: all map keys should be PUSHable"
Right Dict (ConstantScope k)
Dict -> case CheckScope (ConstantScope v) =>
Either BadTypeForScope (Dict (ConstantScope v))
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 ret.
(WithDeMorganScope HasNoOp 'TMap k v, HasNoOp ('TMap k v)) =>
((HasNoOp k, HasNoOp v) => ret) -> ret
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
$
let handleMap
:: Instr s ('T.TMap tk tv ': s) -> (Value tk, Value tv)
-> Maybe (Instr s ('T.TMap tk tv ': s))
handleMap :: 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 (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Value ('TOption v)
-> Instr ('TMap k v : s) ('TOption v : 'TMap k v : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Value k
-> Instr
('TOption v : 'TMap k v : s) (k : 'TOption v : 'TMap k v : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (k : 'TOption v : 'TMap k v : s) ('TMap k v : s)
forall (c :: T) (s :: [T]).
UpdOp c =>
Instr (UpdOpKey c : UpdOpParams c : c : s) (c : s)
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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Value k
-> Instr
('TOption v : 'TMap k v : s) (k : 'TOption v : 'TMap k v : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
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 (a :: [T]) (s :: [T]) (c :: [T]).
Instr a s -> Instr s c -> Instr a c
`Seq` Instr (k : 'TOption v : 'TMap k v : s) ('TMap k v : s)
forall (c :: T) (s :: [T]).
UpdOp c =>
Instr (UpdOpKey c : UpdOpParams c : c : s) (c : s)
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 (heavy :: T) (st :: T) (s :: [T]).
(StorageScope heavy, StorageScope st) =>
Value heavy
-> Instr (heavy : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value t
v Instr (t : s) (t : s)
forall (s :: [T]). Instr s s
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 (a :: T) (b :: T) (s :: [T]).
(SingI a, SingI b, Comparable a) =>
Instr s ('TMap a b : s)
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 (heavy :: T) (st :: T) (s :: [T]).
(StorageScope heavy, StorageScope st) =>
Value heavy
-> Instr (heavy : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value t
v Instr (t : s) (t : s)
forall (s :: [T]). Instr s s
Nop