module Morley.Michelson.Typed.Util
(
DfsSettings (..)
, CtorEffectsApp (..)
, dfsTraverseInstr
, dfsFoldInstr
, dfsModifyInstr
, isMichelsonInstr
, linearizeLeft
, linearizeLeftDeep
, dfsFoldMapValue
, dfsFoldMapValueM
, dfsMapValue
, dfsTraverseValue
, isStringValue
, isBytesValue
, allAtomicValues
, PushableStorageSplit (..)
, splitPushableStorage
, analyzeInstrFailure
, SomeAnns(..)
, instrAnns
) where
import Prelude hiding (Ordering(..))
import Control.Monad.Writer.Strict (Writer, execWriterT, runWriter, tell, writer)
import Data.Constraint (Dict(..), (\\))
import Data.Default (Default(..))
import Data.Generics (listify)
import Data.Map qualified as M
import Data.Set qualified as S
import Fmt (Buildable(..))
import Language.Haskell.TH qualified as TH
import Morley.Michelson.Text (MText)
import Morley.Michelson.Typed.Aliases
import Morley.Michelson.Typed.Annotation
import Morley.Michelson.Typed.ClassifiedInstr
import Morley.Michelson.Typed.Contract
import Morley.Michelson.Typed.Instr
import Morley.Michelson.Typed.Scope
import Morley.Michelson.Typed.T qualified as T
import Morley.Michelson.Typed.Value
import Morley.Michelson.Typed.View
import Morley.Michelson.Untyped (AnyAnn)
data DfsSettings m = DfsSettings
{ forall (m :: * -> *). DfsSettings m -> Bool
dsGoToValues :: Bool
, forall (m :: * -> *). DfsSettings m -> CtorEffectsApp m
dsCtorEffectsApp :: CtorEffectsApp m
, forall (m :: * -> *).
DfsSettings m
-> forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsInstrStep :: (forall i o. Instr i o -> m (Instr i o))
, forall (m :: * -> *).
DfsSettings m -> forall (t' :: T). Value t' -> m (Value t')
dsValueStep :: (forall t'. Value t' -> m (Value t'))
}
data CtorEffectsApp m = CtorEffectsApp
{ forall (m :: * -> *). CtorEffectsApp m -> Text
ceaName :: Text
, forall (m :: * -> *).
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
Monad m =>
Instr i o -> m (Instr i o) -> m (Instr i o)
ceaPostStep
:: forall i o. Monad m
=> Instr i o
-> m (Instr i o)
-> m (Instr i o)
}
instance Buildable (CtorEffectsApp x) where
build :: CtorEffectsApp x -> Doc
build CtorEffectsApp{Text
forall (i :: [T]) (o :: [T]).
Monad x =>
Instr i o -> x (Instr i o) -> x (Instr i o)
ceaName :: forall (m :: * -> *). CtorEffectsApp m -> Text
ceaPostStep :: forall (m :: * -> *).
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
Monad m =>
Instr i o -> m (Instr i o) -> m (Instr i o)
ceaName :: Text
ceaPostStep :: forall (i :: [T]) (o :: [T]).
Monad x =>
Instr i o -> x (Instr i o) -> x (Instr i o)
..} = Text -> Doc
forall a. Buildable a => a -> Doc
build Text
ceaName
instance (Applicative x) => Default (DfsSettings x) where
def :: DfsSettings x
def = DfsSettings
{ dsGoToValues :: Bool
dsGoToValues = Bool
False
, dsCtorEffectsApp :: CtorEffectsApp x
dsCtorEffectsApp = CtorEffectsApp
{ ceaName :: Text
ceaName = Text
"Do nothing"
, ceaPostStep :: forall (i :: [T]) (o :: [T]).
Monad x =>
Instr i o -> x (Instr i o) -> x (Instr i o)
ceaPostStep = (x (Instr i o) -> x (Instr i o))
-> Instr i o -> x (Instr i o) -> x (Instr i o)
forall a b. a -> b -> a
const x (Instr i o) -> x (Instr i o)
forall a. a -> a
id
}
, dsInstrStep :: forall (i :: [T]) (o :: [T]). Instr i o -> x (Instr i o)
dsInstrStep = Instr i o -> x (Instr i o)
forall (i :: [T]) (o :: [T]). Instr i o -> x (Instr i o)
forall a. a -> x a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
, dsValueStep :: forall (t' :: T). Value t' -> x (Value t')
dsValueStep = Value t' -> x (Value t')
forall a. a -> x a
forall (t' :: T). Value t' -> x (Value t')
forall (f :: * -> *) a. Applicative f => a -> f a
pure
}
dfsTraverseInstr ::
forall m inp out.
(Monad m)
=> DfsSettings m
-> Instr inp out
-> m (Instr inp out)
dfsTraverseInstr :: forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr settings :: DfsSettings m
settings@DfsSettings{Bool
CtorEffectsApp m
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
forall (t' :: T). Value t' -> m (Value t')
dsGoToValues :: forall (m :: * -> *). DfsSettings m -> Bool
dsCtorEffectsApp :: forall (m :: * -> *). DfsSettings m -> CtorEffectsApp m
dsInstrStep :: forall (m :: * -> *).
DfsSettings m
-> forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsValueStep :: forall (m :: * -> *).
DfsSettings m -> forall (t' :: T). Value t' -> m (Value t')
dsGoToValues :: Bool
dsCtorEffectsApp :: CtorEffectsApp m
dsInstrStep :: forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsValueStep :: forall (t' :: T). Value t' -> m (Value t')
..} Instr inp out
i = Instr inp out
i Instr inp out
-> (Instr inp out -> m (Instr inp out)) -> m (Instr inp out)
forall a b. a -> (a -> b) -> b
& (forall (cls :: InstrClass).
(SingI cls, WCIConstraint Instr cls) =>
Sing (GetClassified cls)
-> ClassifiedInstr cls inp out -> m (Instr inp out))
-> Instr inp out -> m (Instr inp out)
forall t (inp :: [T]) (out :: [T]) r.
ClassifyInstr t =>
(forall (cls :: InstrClass).
(SingI cls, WCIConstraint Instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r)
-> Instr inp out -> r
forall (instr :: [T] -> [T] -> *) t (inp :: [T]) (out :: [T]) r.
(WithClassifiedInstr instr, ClassifyInstr t) =>
(forall (cls :: InstrClass).
(SingI cls, WCIConstraint instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r)
-> instr inp out -> r
withClassifiedInstr \case
Sing (GetClassified cls)
SingNumChildren (GetClassified cls)
SMayHaveChildren -> \case
C_Ext (TEST_ASSERT (TestAssert Text
nm PrintComment inp
pc Instr inp ('TBool : out)
i1)) ->
(Instr inp ('TBool : out) -> Instr inp out)
-> Instr inp ('TBool : out) -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 (ExtInstr inp -> Instr inp inp
ExtInstr inp -> Instr inp out
forall (inp :: [T]). ExtInstr inp -> Instr inp inp
Ext (ExtInstr inp -> Instr inp out)
-> (Instr inp ('TBool : out) -> ExtInstr inp)
-> Instr inp ('TBool : out)
-> Instr inp out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestAssert inp -> ExtInstr inp
forall (s :: [T]). TestAssert s -> ExtInstr s
TEST_ASSERT (TestAssert inp -> ExtInstr inp)
-> (Instr inp ('TBool : out) -> TestAssert inp)
-> Instr inp ('TBool : out)
-> ExtInstr inp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text
-> PrintComment inp -> Instr inp ('TBool : out) -> TestAssert inp
forall (s :: [T]) (out :: [T]).
Text -> PrintComment s -> Instr s ('TBool : out) -> TestAssert s
TestAssert Text
nm PrintComment inp
pc) Instr inp ('TBool : out)
i1
C_Ext ExtInstr inp
_ -> Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
Sing (GetClassified cls)
SingNumChildren (GetClassified cls)
STwoChildren -> \case
C_Seq Instr inp b1
i1 Instr b1 out
i2 -> (Instr inp b1 -> Instr b1 out -> Instr inp out)
-> Instr inp b1 -> Instr b1 out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]) (i1 :: [T]) (o1 :: [T]) (i2 :: [T])
(o2 :: [T]).
(Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> m (Instr i o)
recursion2 Instr inp b1 -> Instr b1 out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr inp b1
i1 Instr b1 out
i2
C_IF_NONE Instr s out
i1 Instr (a1 : s) out
i2 -> (Instr s out -> Instr (a1 : s) out -> Instr inp out)
-> Instr s out -> Instr (a1 : s) out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]) (i1 :: [T]) (o1 :: [T]) (i2 :: [T])
(o2 :: [T]).
(Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> m (Instr i o)
recursion2 Instr s out -> Instr (a1 : s) out -> Instr inp out
Instr s out -> Instr (a1 : s) out -> Instr ('TOption a1 : s) out
forall (s :: [T]) (out :: [T]) (a :: T).
Instr s out -> Instr (a : s) out -> Instr ('TOption a : s) out
IF_NONE Instr s out
i1 Instr (a1 : s) out
i2
C_IF_LEFT Instr (a1 : s) out
i1 Instr (b1 : s) out
i2 -> (Instr (a1 : s) out -> Instr (b1 : s) out -> Instr inp out)
-> Instr (a1 : s) out -> Instr (b1 : s) out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]) (i1 :: [T]) (o1 :: [T]) (i2 :: [T])
(o2 :: [T]).
(Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> m (Instr i o)
recursion2 Instr (a1 : s) out -> Instr (b1 : s) out -> Instr inp out
Instr (a1 : s) out
-> Instr (b1 : s) out -> Instr ('TOr a1 b1 : s) out
forall (a :: T) (s :: [T]) (out :: [T]) (b :: T).
Instr (a : s) out -> Instr (b : s) out -> Instr ('TOr a b : s) out
IF_LEFT Instr (a1 : s) out
i1 Instr (b1 : s) out
i2
C_IF_CONS Instr (a1 : 'TList a1 : s) out
i1 Instr s out
i2 -> (Instr (a1 : 'TList a1 : s) out -> Instr s out -> Instr inp out)
-> Instr (a1 : 'TList a1 : s) out
-> Instr s out
-> m (Instr inp out)
forall (i :: [T]) (o :: [T]) (i1 :: [T]) (o1 :: [T]) (i2 :: [T])
(o2 :: [T]).
(Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> m (Instr i o)
recursion2 Instr (a1 : 'TList a1 : s) out -> Instr s out -> Instr inp out
Instr (a1 : 'TList a1 : s) out
-> Instr s out -> Instr ('TList a1 : s) out
forall (a :: T) (s :: [T]) (out :: [T]).
Instr (a : 'TList a : s) out
-> Instr s out -> Instr ('TList a : s) out
IF_CONS Instr (a1 : 'TList a1 : s) out
i1 Instr s out
i2
C_IF Instr s out
i1 Instr s out
i2 -> (Instr s out -> Instr s out -> Instr inp out)
-> Instr s out -> Instr s out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]) (i1 :: [T]) (o1 :: [T]) (i2 :: [T])
(o2 :: [T]).
(Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> m (Instr i o)
recursion2 Instr s out -> Instr s out -> Instr inp out
Instr s out -> Instr s out -> Instr ('TBool : s) out
forall (s :: [T]) (out :: [T]).
Instr s out -> Instr s out -> Instr ('TBool : s) out
IF Instr s out
i1 Instr s out
i2
Sing (GetClassified cls)
SingNumChildren (GetClassified cls)
SOneChild -> \case
C_WithLoc ErrorSrcPos
loc Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 (ErrorSrcPos -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
ErrorSrcPos -> Instr inp out -> Instr inp out
WithLoc ErrorSrcPos
loc) Instr inp out
i1
C_Meta SomeMeta
meta Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 (SomeMeta -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
SomeMeta -> Instr inp out -> Instr inp out
Meta SomeMeta
meta) Instr inp out
i1
C_Nested Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
Nested Instr inp out
i1
C_DocGroup DocGrouping
dg Instr inp out
i1 -> (Instr inp out -> Instr inp out)
-> Instr inp out -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 (DocGrouping -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
DocGrouping -> Instr inp out -> Instr inp out
DocGroup DocGrouping
dg) Instr inp out
i1
C_AnnMAP AnnVar
ann Instr (MapOpInp c1 : s) (b1 : s)
i1 -> (Instr (MapOpInp c1 : s) (b1 : s) -> Instr inp out)
-> Instr (MapOpInp c1 : s) (b1 : s) -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 (AnnVar
-> Instr (MapOpInp c1 : s) (b1 : s)
-> Instr (c1 : s) (MapOpRes c1 b1 : s)
forall (c :: T) (b :: T) (s :: [T]).
(MapOp c, SingI b) =>
AnnVar
-> Instr (MapOpInp c : s) (b : s)
-> Instr (c : s) (MapOpRes c b : s)
AnnMAP AnnVar
ann) Instr (MapOpInp c1 : s) (b1 : s)
i1
C_ITER Instr (IterOpEl c1 : out) out
i1 -> (Instr (IterOpEl c1 : out) out -> Instr inp out)
-> Instr (IterOpEl c1 : out) out -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 Instr (IterOpEl c1 : out) out -> Instr inp out
Instr (IterOpEl c1 : out) out -> Instr (c1 : out) out
forall (c :: T) (out :: [T]).
IterOp c =>
Instr (IterOpEl c : out) out -> Instr (c : out) out
ITER Instr (IterOpEl c1 : out) out
i1
C_LOOP Instr out ('TBool : out)
i1 -> (Instr out ('TBool : out) -> Instr inp out)
-> Instr out ('TBool : out) -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 Instr out ('TBool : out) -> Instr inp out
Instr out ('TBool : out) -> Instr ('TBool : out) out
forall (out :: [T]).
Instr out ('TBool : out) -> Instr ('TBool : out) out
LOOP Instr out ('TBool : out)
i1
C_LOOP_LEFT Instr (a1 : s) ('TOr a1 b1 : s)
i1 -> (Instr (a1 : s) ('TOr a1 b1 : s) -> Instr inp out)
-> Instr (a1 : s) ('TOr a1 b1 : s) -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 Instr (a1 : s) ('TOr a1 b1 : s) -> Instr inp out
Instr (a1 : s) ('TOr a1 b1 : s) -> Instr ('TOr a1 b1 : s) (b1 : 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 (a1 : s) ('TOr a1 b1 : s)
i1
C_DIP Instr a1 c1
i1 -> (Instr a1 c1 -> Instr inp out) -> Instr a1 c1 -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 Instr a1 c1 -> Instr inp out
Instr a1 c1 -> Instr (b1 : a1) (b1 : c1)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr a1 c1
i1
C_DIPN PeanoNatural n
s Instr s s'
i1 -> (Instr s s' -> Instr inp out) -> Instr s s' -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 (PeanoNatural n -> Instr s s' -> Instr inp out
forall (n :: Peano) (inp :: [T]) (out :: [T]) (s :: [T])
(s' :: [T]).
ConstraintDIPN n inp out s s' =>
PeanoNatural n -> Instr s s' -> Instr inp out
DIPN PeanoNatural n
s) Instr s s'
i1
Sing (GetClassified cls)
SingNumChildren (GetClassified cls)
SHasIndirectChildren
| Bool
dsGoToValues -> \case
C_AnnPUSH Anns '[VarAnn, Notes t]
ann Value' Instr t
v -> CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
Monad m =>
Instr i o -> m (Instr i o) -> m (Instr i o)
forall (m :: * -> *).
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
Monad m =>
Instr i o -> m (Instr i o) -> m (Instr i o)
ceaPostStep CtorEffectsApp m
dsCtorEffectsApp Instr inp out
i do
Value' Instr t
innerV <- DfsSettings m -> Value' Instr t -> m (Value' Instr t)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
settings Value' Instr t
v
Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsInstrStep (Instr inp out -> m (Instr inp out))
-> Instr inp out -> m (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Anns '[VarAnn, Notes t] -> Value' Instr t -> Instr inp (t : inp)
forall (t :: T) (inp :: [T]).
ConstantScope t =>
Anns '[VarAnn, Notes t] -> Value' Instr t -> Instr inp (t : inp)
AnnPUSH Anns '[VarAnn, Notes t]
ann Value' Instr t
innerV
C_AnnLAMBDA Anns '[VarAnn, Notes i, Notes o]
ann RemFail Instr '[i] '[o]
i1 ->
(Instr '[i] '[o] -> Instr inp out)
-> Instr '[i] '[o] -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 (Anns '[VarAnn, Notes i, Notes o]
-> RemFail Instr '[i] '[o] -> Instr inp ('TLambda i o : inp)
forall (i :: T) (o :: T) (inp :: [T]).
(SingI i, SingI o) =>
Anns '[VarAnn, Notes i, Notes o]
-> RemFail Instr '[i] '[o] -> Instr inp ('TLambda i o : inp)
AnnLAMBDA Anns '[VarAnn, Notes i, Notes o]
ann (RemFail Instr '[i] '[o] -> Instr inp out)
-> (Instr '[i] '[o] -> RemFail Instr '[i] '[o])
-> Instr '[i] '[o]
-> Instr inp out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr '[i] '[o] -> RemFail Instr '[i] '[o]
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
analyzeInstrFailure) (RemFail Instr '[i] '[o] -> Instr '[i] '[o]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
RemFail instr i o -> instr i o
rfAnyInstr RemFail Instr '[i] '[o]
i1)
C_AnnLAMBDA_REC Anns '[VarAnn, Notes i, Notes o]
ann RemFail Instr '[i, 'TLambda i o] '[o]
i1 ->
(Instr '[i, 'TLambda i o] '[o] -> Instr inp out)
-> Instr '[i, 'TLambda i o] '[o] -> m (Instr inp out)
forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 (Anns '[VarAnn, Notes i, Notes o]
-> RemFail Instr '[i, 'TLambda i o] '[o]
-> Instr inp ('TLambda i o : inp)
forall (i :: T) (o :: T) (inp :: [T]).
(SingI i, SingI o) =>
Anns '[VarAnn, Notes i, Notes o]
-> RemFail Instr '[i, 'TLambda i o] '[o]
-> Instr inp ('TLambda i o : inp)
AnnLAMBDA_REC Anns '[VarAnn, Notes i, Notes o]
ann (RemFail Instr '[i, 'TLambda i o] '[o] -> Instr inp out)
-> (Instr '[i, 'TLambda i o] '[o]
-> RemFail Instr '[i, 'TLambda i o] '[o])
-> Instr '[i, 'TLambda i o] '[o]
-> Instr inp out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr '[i, 'TLambda i o] '[o]
-> RemFail Instr '[i, 'TLambda i o] '[o]
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
analyzeInstrFailure) (RemFail Instr '[i, 'TLambda i o] '[o]
-> Instr '[i, 'TLambda i o] '[o]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
RemFail instr i o -> instr i o
rfAnyInstr RemFail Instr '[i, 'TLambda i o] '[o]
i1)
C_AnnCREATE_CONTRACT Anns '[VarAnn, VarAnn]
ann contract :: Contract' Instr p g
contract@Contract{EntriesOrder
Notes g
ViewsSet' Instr g
ParamNotes p
ContractCode' Instr p g
cCode :: ContractCode' Instr p g
cParamNotes :: ParamNotes p
cStoreNotes :: Notes g
cViews :: ViewsSet' Instr g
cEntriesOrder :: EntriesOrder
cCode :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> ContractCode' instr cp st
cParamNotes :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> ParamNotes cp
cStoreNotes :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> Notes st
cViews :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> ViewsSet' instr st
cEntriesOrder :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> EntriesOrder
..} ->
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
Monad m =>
Instr i o -> m (Instr i o) -> m (Instr i o)
forall (m :: * -> *).
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
Monad m =>
Instr i o -> m (Instr i o) -> m (Instr i o)
ceaPostStep CtorEffectsApp m
dsCtorEffectsApp Instr inp out
i
case ContractCode' Instr p g
cCode of
ContractCode Instr (ContractInp p g) (ContractOut g)
c -> do
Instr (ContractInp p g) (ContractOut g)
codeI <- DfsSettings m
-> Instr (ContractInp p g) (ContractOut g)
-> m (Instr (ContractInp p g) (ContractOut g))
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings m
settings Instr (ContractInp p g) (ContractOut g)
c
Map ViewName (SomeView' Instr g)
viewsI <- Map ViewName (SomeView' Instr g)
-> (SomeView' Instr g -> m (SomeView' Instr g))
-> m (Map ViewName (SomeView' Instr g))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (ViewsSet' Instr g -> Map ViewName (SomeView' Instr g)
forall (instr :: [T] -> [T] -> *) (st :: T).
ViewsSet' instr st -> Map ViewName (SomeView' instr st)
unViewsSet ViewsSet' Instr g
cViews) \(SomeView v :: View' Instr arg g ret
v@View{ViewName
Notes arg
Notes ret
ViewCode' Instr arg g ret
vName :: ViewName
vArgument :: Notes arg
vReturn :: Notes ret
vCode :: ViewCode' Instr arg g ret
vName :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> ViewName
vArgument :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> Notes arg
vReturn :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> Notes ret
vCode :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> ViewCode' instr arg st ret
..}) -> do
ViewCode' Instr arg g ret
code <- DfsSettings m
-> ViewCode' Instr arg g ret -> m (ViewCode' Instr arg g ret)
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings m
settings ViewCode' Instr arg g ret
vCode
pure $ 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
code }
Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsInstrStep (Instr inp out -> m (Instr inp out))
-> Instr inp out -> m (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Anns '[VarAnn, VarAnn]
-> Contract' Instr p g
-> Instr
('TOption 'TKeyHash : 'TMutez : g : s)
('TOperation : 'TAddress : s)
forall (p :: T) (g :: T) (s :: [T]).
(ParameterScope p, StorageScope g, IsNotInView) =>
Anns '[VarAnn, VarAnn]
-> Contract' Instr p g
-> Instr
('TOption 'TKeyHash : 'TMutez : g : s)
('TOperation : 'TAddress : s)
AnnCREATE_CONTRACT Anns '[VarAnn, VarAnn]
ann (Contract' Instr p g
-> Instr
('TOption 'TKeyHash : 'TMutez : g : s)
('TOperation : 'TAddress : s))
-> Contract' Instr p g
-> Instr
('TOption 'TKeyHash : 'TMutez : g : s)
('TOperation : 'TAddress : s)
forall a b. (a -> b) -> a -> b
$ Contract' Instr p g
contract
{ cCode :: ContractCode' Instr p g
cCode = Instr (ContractInp p g) (ContractOut g) -> ContractCode' Instr p g
forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
instr (ContractInp cp st) (ContractOut st)
-> ContractCode' instr cp st
ContractCode Instr (ContractInp p g) (ContractOut g)
codeI
, cViews :: ViewsSet' Instr g
cViews = Map ViewName (SomeView' Instr g) -> ViewsSet' Instr g
forall (instr :: [T] -> [T] -> *) (st :: T).
Map ViewName (SomeView' instr st) -> ViewsSet' instr st
ViewsSet Map ViewName (SomeView' Instr g)
viewsI
}
| Bool
otherwise -> m (Instr inp out)
-> ClassifiedInstr cls inp out -> m (Instr inp out)
forall a b. a -> b -> a
const (m (Instr inp out)
-> ClassifiedInstr cls inp out -> m (Instr inp out))
-> m (Instr inp out)
-> ClassifiedInstr cls inp out
-> m (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
Sing (GetClassified cls)
SingNumChildren (GetClassified cls)
SNoChildren -> m (Instr inp out)
-> ClassifiedInstr cls inp out -> m (Instr inp out)
forall a b. a -> b -> a
const (m (Instr inp out)
-> ClassifiedInstr cls inp out -> m (Instr inp out))
-> m (Instr inp out)
-> ClassifiedInstr cls inp out
-> m (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out -> m (Instr inp out)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr inp out
i
where
recursion0 ::
forall a b. Instr a b -> m (Instr a b)
recursion0 :: forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
recursion0 Instr a b
i0 =
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
Monad m =>
Instr i o -> m (Instr i o) -> m (Instr i o)
forall (m :: * -> *).
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
Monad m =>
Instr i o -> m (Instr i o) -> m (Instr i o)
ceaPostStep CtorEffectsApp m
dsCtorEffectsApp Instr a b
i0 (m (Instr a b) -> m (Instr a b)) -> m (Instr a b) -> m (Instr a b)
forall a b. (a -> b) -> a -> b
$
Instr a b -> m (Instr a b)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsInstrStep Instr a b
i0
recursion1 ::
forall a b c d. (Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 :: forall (a :: [T]) (b :: [T]) (c :: [T]) (d :: [T]).
(Instr a b -> Instr c d) -> Instr a b -> m (Instr c d)
recursion1 Instr a b -> Instr c d
constructor Instr a b
i0 =
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
Monad m =>
Instr i o -> m (Instr i o) -> m (Instr i o)
forall (m :: * -> *).
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
Monad m =>
Instr i o -> m (Instr i o) -> m (Instr i o)
ceaPostStep CtorEffectsApp m
dsCtorEffectsApp (Instr a b -> Instr c d
constructor Instr a b
i0) do
Instr a b
innerI <- DfsSettings m -> Instr a b -> m (Instr a b)
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings m
settings Instr a b
i0
Instr c d -> m (Instr c d)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsInstrStep (Instr c d -> m (Instr c d)) -> Instr c d -> m (Instr c d)
forall a b. (a -> b) -> a -> b
$ Instr a b -> Instr c d
constructor Instr a b
innerI
recursion2 ::
forall i o i1 o1 i2 o2.
(Instr i1 o1 -> Instr i2 o2 -> Instr i o) ->
Instr i1 o1 -> Instr i2 o2 -> m (Instr i o)
recursion2 :: forall (i :: [T]) (o :: [T]) (i1 :: [T]) (o1 :: [T]) (i2 :: [T])
(o2 :: [T]).
(Instr i1 o1 -> Instr i2 o2 -> Instr i o)
-> Instr i1 o1 -> Instr i2 o2 -> m (Instr i o)
recursion2 Instr i1 o1 -> Instr i2 o2 -> Instr i o
constructor Instr i1 o1
i1 Instr i2 o2
i2 =
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
Monad m =>
Instr i o -> m (Instr i o) -> m (Instr i o)
forall (m :: * -> *).
CtorEffectsApp m
-> forall (i :: [T]) (o :: [T]).
Monad m =>
Instr i o -> m (Instr i o) -> m (Instr i o)
ceaPostStep CtorEffectsApp m
dsCtorEffectsApp (Instr i1 o1 -> Instr i2 o2 -> Instr i o
constructor Instr i1 o1
i1 Instr i2 o2
i2) do
Instr i1 o1
i1' <- DfsSettings m -> Instr i1 o1 -> m (Instr i1 o1)
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings m
settings Instr i1 o1
i1
Instr i2 o2
i2' <- DfsSettings m -> Instr i2 o2 -> m (Instr i2 o2)
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings m
settings Instr i2 o2
i2
Instr i o -> m (Instr i o)
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsInstrStep (Instr i o -> m (Instr i o)) -> Instr i o -> m (Instr i o)
forall a b. (a -> b) -> a -> b
$ Instr i1 o1 -> Instr i2 o2 -> Instr i o
constructor Instr i1 o1
i1' Instr i2 o2
i2'
dfsFoldInstr
:: forall x inp out.
(Monoid x)
=> DfsSettings (Writer x)
-> (forall i o. Instr i o -> x)
-> Instr inp out
-> x
dfsFoldInstr :: forall x (inp :: [T]) (out :: [T]).
Monoid x =>
DfsSettings (Writer x)
-> (forall (i :: [T]) (o :: [T]). Instr i o -> x)
-> Instr inp out
-> x
dfsFoldInstr DfsSettings (WriterT x Identity)
settings forall (i :: [T]) (o :: [T]). Instr i o -> x
step =
(Instr inp out, x) -> x
forall a b. (a, b) -> b
snd ((Instr inp out, x) -> x)
-> (Instr inp out -> (Instr inp out, x)) -> Instr inp out -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Writer x (Instr inp out) -> (Instr inp out, x)
forall w a. Writer w a -> (a, w)
runWriter (Writer x (Instr inp out) -> (Instr inp out, x))
-> (Instr inp out -> Writer x (Instr inp out))
-> Instr inp out
-> (Instr inp out, x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DfsSettings (WriterT x Identity)
-> Instr inp out -> Writer x (Instr inp out)
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings (WriterT x Identity)
settings{dsInstrStep :: forall (i :: [T]) (o :: [T]). Instr i o -> Writer x (Instr i o)
dsInstrStep = (Instr i o, x) -> WriterT x Identity (Instr i o)
forall a. (a, x) -> WriterT x Identity a
forall w (m :: * -> *) a. MonadWriter w m => (a, w) -> m a
writer ((Instr i o, x) -> WriterT x Identity (Instr i o))
-> (Instr i o -> (Instr i o, x))
-> Instr i o
-> WriterT x Identity (Instr i o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Instr i o -> Instr i o
forall a. a -> a
id (Instr i o -> Instr i o)
-> (Instr i o -> x) -> Instr i o -> (Instr i o, x)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Instr i o -> x
forall (i :: [T]) (o :: [T]). Instr i o -> x
step)}
dfsModifyInstr
:: DfsSettings Identity
-> (forall i o. Instr i o -> Instr i o)
-> Instr inp out
-> Instr inp out
dfsModifyInstr :: forall (inp :: [T]) (out :: [T]).
DfsSettings Identity
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
dfsModifyInstr DfsSettings Identity
settings forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
step =
Identity (Instr inp out) -> Instr inp out
forall a. Identity a -> a
runIdentity (Identity (Instr inp out) -> Instr inp out)
-> (Instr inp out -> Identity (Instr inp out))
-> Instr inp out
-> Instr inp out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DfsSettings Identity -> Instr inp out -> Identity (Instr inp out)
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings Identity
settings{dsInstrStep :: forall (i :: [T]) (o :: [T]). Instr i o -> Identity (Instr i o)
dsInstrStep = (Instr i o -> Identity (Instr i o)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Instr i o -> Identity (Instr i o))
-> (Instr i o -> Instr i o) -> Instr i o -> Identity (Instr i o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr i o -> Instr i o
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
step)}
analyzeInstrFailure :: Instr i o -> RemFail Instr i o
analyzeInstrFailure :: forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
analyzeInstrFailure = Instr i o -> RemFail Instr i o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go
where
go :: Instr i o -> RemFail Instr i o
go :: forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr i o
i' = Instr i o
i' Instr i o -> (Instr i o -> RemFail Instr i o) -> RemFail Instr i o
forall a b. a -> (a -> b) -> b
& (forall (cls :: InstrClass).
(SingI cls, WCIConstraint Instr cls) =>
Sing (GetClassified cls)
-> ClassifiedInstr cls i o -> RemFail Instr i o)
-> Instr i o -> RemFail Instr i o
forall t (inp :: [T]) (out :: [T]) r.
ClassifyInstr t =>
(forall (cls :: InstrClass).
(SingI cls, WCIConstraint Instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r)
-> Instr inp out -> r
forall (instr :: [T] -> [T] -> *) t (inp :: [T]) (out :: [T]) r.
(WithClassifiedInstr instr, ClassifyInstr t) =>
(forall (cls :: InstrClass).
(SingI cls, WCIConstraint instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r)
-> instr inp out -> r
withClassifiedInstr \case
Sing (GetClassified cls)
SingFailureType (GetClassified cls)
SAlwaysFailing -> \case
ClassifiedInstr cls i o
C_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 Instr i o'
Instr (a1 : s) o'
forall (o' :: [T]). Instr i o'
forall (a :: T) (s :: [T]) (out :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : s) out
FAILWITH
ClassifiedInstr cls i o
C_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 Instr i o'
Instr ('TNever : s) o'
forall (o' :: [T]). Instr i o'
forall (s :: [T]) (out :: [T]). Instr ('TNever : s) out
NEVER
Sing (GetClassified cls)
SingFailureType (GetClassified cls)
SFailingNormal -> (forall (cls :: InstrClass).
(SingI cls, WCIConstraint (ClassifiedInstr cls) cls) =>
Sing (GetClassified cls)
-> ClassifiedInstr cls i o -> RemFail Instr i o)
-> ClassifiedInstr cls i o -> RemFail Instr i o
forall t (inp :: [T]) (out :: [T]) r.
ClassifyInstr t =>
(forall (cls :: InstrClass).
(SingI cls, WCIConstraint (ClassifiedInstr cls) cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r)
-> ClassifiedInstr cls inp out -> r
forall (instr :: [T] -> [T] -> *) t (inp :: [T]) (out :: [T]) r.
(WithClassifiedInstr instr, ClassifyInstr t) =>
(forall (cls :: InstrClass).
(SingI cls, WCIConstraint instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r)
-> instr inp out -> r
withClassifiedInstr \case
Sing (GetClassified cls)
SingNumChildren (GetClassified cls)
SNoChildren -> RemFail Instr i o -> ClassifiedInstr cls i o -> RemFail Instr i o
forall a b. a -> b -> a
const (RemFail Instr i o -> ClassifiedInstr cls i o -> RemFail Instr i o)
-> RemFail Instr i o
-> ClassifiedInstr cls i o
-> RemFail Instr i o
forall a b. (a -> b) -> a -> b
$ Instr i o -> RemFail Instr i o
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i'
Sing (GetClassified cls)
SingNumChildren (GetClassified cls)
SHasIndirectChildren -> RemFail Instr i o -> ClassifiedInstr cls i o -> RemFail Instr i o
forall a b. a -> b -> a
const (RemFail Instr i o -> ClassifiedInstr cls i o -> RemFail Instr i o)
-> RemFail Instr i o
-> ClassifiedInstr cls i o
-> RemFail Instr i o
forall a b. (a -> b) -> a -> b
$ Instr i o -> RemFail Instr i o
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i'
Sing (GetClassified cls)
SingNumChildren (GetClassified cls)
SMayHaveChildren -> \case
C_Ext ExtInstr i
_ -> Instr i o -> RemFail Instr i o
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i'
Sing (GetClassified cls)
SingNumChildren (GetClassified cls)
STwoChildren -> \case
C_Seq Instr i b1
a Instr b1 o
b -> Instr i b1 -> Instr b1 o' -> Instr i o'
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr i b1
a (forall {o' :: [T]}. Instr b1 o' -> Instr i o')
-> RemFail Instr b1 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 b1 o -> RemFail Instr b1 o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr b1 o
b
C_IF_NONE Instr s o
l Instr (a1 : s) o
r -> (forall (o' :: [T]). Instr s o' -> Instr (a1 : s) o' -> Instr i o')
-> RemFail Instr s o
-> RemFail Instr (a1 : 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 Instr s o' -> Instr (a1 : s) o' -> Instr i o'
Instr s o' -> Instr (a1 : s) o' -> Instr ('TOption a1 : s) o'
forall (o' :: [T]). Instr s o' -> Instr (a1 : s) o' -> Instr i o'
forall (s :: [T]) (out :: [T]) (a :: T).
Instr s out -> Instr (a : s) out -> Instr ('TOption a : s) out
IF_NONE (Instr s o -> RemFail Instr s o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr s o
l) (Instr (a1 : s) o -> RemFail Instr (a1 : s) o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr (a1 : s) o
r)
C_IF_LEFT Instr (a1 : s) o
l Instr (b1 : s) o
r -> (forall (o' :: [T]).
Instr (a1 : s) o' -> Instr (b1 : s) o' -> Instr i o')
-> RemFail Instr (a1 : s) o
-> RemFail Instr (b1 : 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 Instr (a1 : s) o' -> Instr (b1 : s) o' -> Instr i o'
Instr (a1 : s) o' -> Instr (b1 : s) o' -> Instr ('TOr a1 b1 : s) o'
forall (o' :: [T]).
Instr (a1 : s) o' -> Instr (b1 : s) o' -> Instr i o'
forall (a :: T) (s :: [T]) (out :: [T]) (b :: T).
Instr (a : s) out -> Instr (b : s) out -> Instr ('TOr a b : s) out
IF_LEFT (Instr (a1 : s) o -> RemFail Instr (a1 : s) o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr (a1 : s) o
l) (Instr (b1 : s) o -> RemFail Instr (b1 : s) o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr (b1 : s) o
r)
C_IF_CONS Instr (a1 : 'TList a1 : s) o
l Instr s o
r -> (forall (o' :: [T]).
Instr (a1 : 'TList a1 : s) o' -> Instr s o' -> Instr i o')
-> RemFail Instr (a1 : 'TList a1 : 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 Instr (a1 : 'TList a1 : s) o' -> Instr s o' -> Instr i o'
Instr (a1 : 'TList a1 : s) o'
-> Instr s o' -> Instr ('TList a1 : s) o'
forall (o' :: [T]).
Instr (a1 : 'TList a1 : s) o' -> Instr s o' -> Instr i o'
forall (a :: T) (s :: [T]) (out :: [T]).
Instr (a : 'TList a : s) out
-> Instr s out -> Instr ('TList a : s) out
IF_CONS (Instr (a1 : 'TList a1 : s) o
-> RemFail Instr (a1 : 'TList a1 : s) o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr (a1 : 'TList a1 : 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)
C_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 Instr s o' -> Instr s o' -> Instr i o'
Instr s o' -> Instr s o' -> Instr ('TBool : s) o'
forall (o' :: [T]). Instr s o' -> Instr s o' -> Instr i o'
forall (s :: [T]) (out :: [T]).
Instr s out -> Instr s out -> Instr ('TBool : s) out
IF (Instr s o -> RemFail Instr s o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr s o
l) (Instr s o -> RemFail Instr s o
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
go Instr s o
r)
Sing (GetClassified cls)
SingNumChildren (GetClassified cls)
SOneChild -> (forall (cls :: InstrClass).
(SingI cls, WCIConstraint (ClassifiedInstr cls) cls) =>
Sing (GetClassified cls)
-> ClassifiedInstr cls i o -> RemFail Instr i o)
-> ClassifiedInstr cls i o -> RemFail Instr i o
forall t (inp :: [T]) (out :: [T]) r.
ClassifyInstr t =>
(forall (cls :: InstrClass).
(SingI cls, WCIConstraint (ClassifiedInstr cls) cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r)
-> ClassifiedInstr cls inp out -> r
forall (instr :: [T] -> [T] -> *) t (inp :: [T]) (out :: [T]) r.
(WithClassifiedInstr instr, ClassifyInstr t) =>
(forall (cls :: InstrClass).
(SingI cls, WCIConstraint instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r)
-> instr inp out -> r
withClassifiedInstr \case
Sing (GetClassified cls)
SingIsMichelson (GetClassified cls)
SFromMichelson -> RemFail Instr i o -> ClassifiedInstr cls i o -> RemFail Instr i o
forall a b. a -> b -> a
const (RemFail Instr i o -> ClassifiedInstr cls i o -> RemFail Instr i o)
-> RemFail Instr i o
-> ClassifiedInstr cls i o
-> RemFail Instr i o
forall a b. (a -> b) -> a -> b
$ Instr i o -> RemFail Instr i o
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr i o
i'
Sing (GetClassified cls)
_ -> \case
C_WithLoc ErrorSrcPos
loc Instr i o
i -> ErrorSrcPos -> Instr i o' -> Instr i o'
forall (inp :: [T]) (out :: [T]).
ErrorSrcPos -> Instr inp out -> Instr inp out
WithLoc ErrorSrcPos
loc (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
C_Meta SomeMeta
meta Instr i o
i -> SomeMeta -> Instr i o' -> Instr i o'
forall (inp :: [T]) (out :: [T]).
SomeMeta -> Instr inp out -> Instr inp out
Meta SomeMeta
meta (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
C_Nested Instr i o
i -> Instr i o' -> Instr i o'
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
C_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
linearizeLeft :: Instr inp out -> Instr inp out
linearizeLeft :: forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
linearizeLeft = Bool -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
Bool -> Instr inp out -> Instr inp out
linearizeLeftHelper Bool
False
where
linearizeLeftHelper :: Bool -> Instr inp out -> Instr inp out
linearizeLeftHelper :: forall (inp :: [T]) (out :: [T]).
Bool -> Instr inp out -> Instr inp out
linearizeLeftHelper Bool
isLeftInstrAlreadyLinear =
\case
Seq Instr inp b
i1 (Seq Instr b b
i2 Instr b out
i3) ->
Bool -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
Bool -> Instr inp out -> Instr inp out
linearizeLeftHelper Bool
True (Instr inp out -> Instr inp out) -> Instr inp out -> Instr inp out
forall a b. (a -> b) -> a -> b
$
Instr inp b -> Instr b out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq (Bool -> Instr inp b -> Instr inp b
forall (inp :: [T]) (out :: [T]).
Bool -> Instr inp out -> Instr inp out
linearizeLeftHelper Bool
isLeftInstrAlreadyLinear (Instr inp b -> Instr b b -> Instr inp b
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr inp b
i1 Instr b b
i2)) Instr b out
i3
Seq Instr inp b
i1 Instr b out
i2
| Bool
isLeftInstrAlreadyLinear
, Instr b out
Nop <- Instr b out
i2 -> Instr inp out
Instr inp b
i1
| Bool
isLeftInstrAlreadyLinear -> Instr inp b -> Instr b out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr inp b
i1 Instr b out
i2
| Instr b out
Nop <- Instr b out
i2 -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
linearizeLeft Instr inp out
Instr inp b
i1
| Bool
otherwise -> Instr inp b -> Instr b out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq (Instr inp b -> Instr inp b
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
linearizeLeft Instr inp b
i1) Instr b out
i2
Instr inp out
i -> Instr inp out
i
linearizeLeftDeep :: Instr inp out -> Instr inp out
linearizeLeftDeep :: forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
linearizeLeftDeep = DfsSettings Identity
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
forall (inp :: [T]) (out :: [T]).
DfsSettings Identity
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
dfsModifyInstr DfsSettings Identity
forall a. Default a => a
def Instr i o -> Instr i o
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
linearizeLeft
dfsMapValue ::
forall t.
DfsSettings Identity
-> Value t
-> Value t
dfsMapValue :: forall (t :: T). DfsSettings Identity -> Value t -> Value t
dfsMapValue DfsSettings Identity
settings Value t
v = Identity (Value t) -> Value t
forall a. Identity a -> a
runIdentity (Identity (Value t) -> Value t) -> Identity (Value t) -> Value t
forall a b. (a -> b) -> a -> b
$ DfsSettings Identity -> Value t -> Identity (Value t)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings Identity
settings Value t
v
dfsTraverseValue ::
forall t m.
(Monad m)
=> DfsSettings m
-> Value t
-> m (Value t)
dfsTraverseValue :: forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue settings :: DfsSettings m
settings@DfsSettings{Bool
CtorEffectsApp m
forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
forall (t' :: T). Value t' -> m (Value t')
dsGoToValues :: forall (m :: * -> *). DfsSettings m -> Bool
dsCtorEffectsApp :: forall (m :: * -> *). DfsSettings m -> CtorEffectsApp m
dsInstrStep :: forall (m :: * -> *).
DfsSettings m
-> forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsValueStep :: forall (m :: * -> *).
DfsSettings m -> forall (t' :: T). Value t' -> m (Value t')
dsGoToValues :: Bool
dsCtorEffectsApp :: CtorEffectsApp m
dsInstrStep :: forall (i :: [T]) (o :: [T]). Instr i o -> m (Instr i o)
dsValueStep :: forall (t' :: T). Value t' -> m (Value t')
..} Value t
i = case Value t
i of
VKey{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
Value t
VUnit -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VSignature{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VChainId{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VOp{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VContract{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VTicket{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VLam LambdaCode' Instr inp out
code -> case LambdaCode' Instr inp out
code of
LambdaCode RemFail Instr '[inp] '[out]
lambda -> do
Value' Instr ('TLambda inp out)
v <- (Instr '[inp] '[out] -> Value' Instr ('TLambda inp out))
-> m (Instr '[inp] '[out]) -> m (Value' Instr ('TLambda inp out))
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (LambdaCode' Instr inp out -> Value' Instr ('TLambda inp out)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI out) =>
LambdaCode' instr inp out -> Value' instr ('TLambda inp out)
VLam (LambdaCode' Instr inp out -> Value' Instr ('TLambda inp out))
-> (Instr '[inp] '[out] -> LambdaCode' Instr inp out)
-> Instr '[inp] '[out]
-> Value' Instr ('TLambda inp out)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RemFail Instr '[inp] '[out] -> LambdaCode' Instr inp out
forall (instr :: [T] -> [T] -> *) (inp :: T) (out :: T).
(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] -> LambdaCode' instr inp out
LambdaCode (RemFail Instr '[inp] '[out] -> LambdaCode' Instr inp out)
-> (Instr '[inp] '[out] -> RemFail Instr '[inp] '[out])
-> Instr '[inp] '[out]
-> LambdaCode' Instr inp out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr '[inp] '[out] -> RemFail Instr '[inp] '[out]
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
analyzeInstrFailure) (m (Instr '[inp] '[out]) -> m (Value' Instr ('TLambda inp out)))
-> m (Instr '[inp] '[out]) -> m (Value' Instr ('TLambda inp out))
forall a b. (a -> b) -> a -> b
$ DfsSettings m -> Instr '[inp] '[out] -> m (Instr '[inp] '[out])
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings m
settings (RemFail Instr '[inp] '[out] -> Instr '[inp] '[out]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
RemFail instr i o -> instr i o
rfAnyInstr RemFail Instr '[inp] '[out]
lambda)
Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
Value' Instr ('TLambda inp out)
v
LambdaCodeRec RemFail Instr '[inp, 'TLambda inp out] '[out]
lambda -> do
Value' Instr ('TLambda inp out)
v <- (Instr '[inp, 'TLambda inp out] '[out]
-> Value' Instr ('TLambda inp out))
-> m (Instr '[inp, 'TLambda inp out] '[out])
-> m (Value' Instr ('TLambda inp out))
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (LambdaCode' Instr inp out -> Value' Instr ('TLambda inp out)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI out) =>
LambdaCode' instr inp out -> Value' instr ('TLambda inp out)
VLam (LambdaCode' Instr inp out -> Value' Instr ('TLambda inp out))
-> (Instr '[inp, 'TLambda inp out] '[out]
-> LambdaCode' Instr inp out)
-> Instr '[inp, 'TLambda inp out] '[out]
-> Value' Instr ('TLambda inp out)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RemFail Instr '[inp, 'TLambda inp out] '[out]
-> LambdaCode' Instr inp out
forall (instr :: [T] -> [T] -> *) (inp :: T) (out :: T).
(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, 'TLambda inp out] '[out]
-> LambdaCode' instr inp out
LambdaCodeRec (RemFail Instr '[inp, 'TLambda inp out] '[out]
-> LambdaCode' Instr inp out)
-> (Instr '[inp, 'TLambda inp out] '[out]
-> RemFail Instr '[inp, 'TLambda inp out] '[out])
-> Instr '[inp, 'TLambda inp out] '[out]
-> LambdaCode' Instr inp out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr '[inp, 'TLambda inp out] '[out]
-> RemFail Instr '[inp, 'TLambda inp out] '[out]
forall (i :: [T]) (o :: [T]). Instr i o -> RemFail Instr i o
analyzeInstrFailure) (m (Instr '[inp, 'TLambda inp out] '[out])
-> m (Value' Instr ('TLambda inp out)))
-> m (Instr '[inp, 'TLambda inp out] '[out])
-> m (Value' Instr ('TLambda inp out))
forall a b. (a -> b) -> a -> b
$ DfsSettings m
-> Instr '[inp, 'TLambda inp out] '[out]
-> m (Instr '[inp, 'TLambda inp out] '[out])
forall (m :: * -> *) (inp :: [T]) (out :: [T]).
Monad m =>
DfsSettings m -> Instr inp out -> m (Instr inp out)
dfsTraverseInstr DfsSettings m
settings (RemFail Instr '[inp, 'TLambda inp out] '[out]
-> Instr '[inp, 'TLambda inp out] '[out]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
RemFail instr i o -> instr i o
rfAnyInstr RemFail Instr '[inp, 'TLambda inp out] '[out]
lambda)
Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
Value' Instr ('TLambda inp out)
v
VInt{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VNat{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VString{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VBytes{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VMutez{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VBool{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VKeyHash{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VBls12381Fr{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VBls12381G1{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VBls12381G2{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VTimestamp{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VAddress{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VChestKey{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VChest{} -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
VOption Maybe (Value' Instr t1)
mVal -> case Maybe (Value' Instr t1)
mVal of
Maybe (Value' Instr t1)
Nothing -> Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep Value t
i
Just Value' Instr t1
val -> (Value' Instr t1 -> Value t) -> Value' Instr t1 -> m (Value t)
forall (t' :: T). (Value t' -> Value t) -> Value t' -> m (Value t)
recursion1 (Maybe (Value' Instr t1) -> Value t
Maybe (Value' Instr t1) -> Value' Instr ('TOption t1)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption (Maybe (Value' Instr t1) -> Value t)
-> (Value' Instr t1 -> Maybe (Value' Instr t1))
-> Value' Instr t1
-> Value t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' Instr t1 -> Maybe (Value' Instr t1)
forall a. a -> Maybe a
Just) Value' Instr t1
val
VList [Value' Instr t1]
vals -> do
[Value' Instr t1]
vs <- (Value' Instr t1 -> m (Value' Instr t1))
-> [Value' Instr t1] -> m [Value' Instr t1]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (DfsSettings m -> Value' Instr t1 -> m (Value' Instr t1)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
settings) [Value' Instr t1]
vals
Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep (Value t -> m (Value t)) -> Value t -> m (Value t)
forall a b. (a -> b) -> a -> b
$ [Value' Instr t1] -> Value' Instr ('TList t1)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
VList [Value' Instr t1]
vs
VSet Set (Value t1)
vals -> do
Set (Value t1)
cs <- [Value t1] -> Set (Value t1)
forall a. Ord a => [a] -> Set a
S.fromList ([Value t1] -> Set (Value t1))
-> m [Value t1] -> m (Set (Value t1))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value t1 -> m (Value t1)) -> [Value t1] -> m [Value t1]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (DfsSettings m -> Value t1 -> m (Value t1)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
settings) (Set (Value t1) -> [Value t1]
forall a. Set a -> [a]
S.toList Set (Value t1)
vals)
Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep (Set (Value t1) -> Value' Instr ('TSet t1)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
Comparable t1 =>
Set (Value' instr t1) -> Value' instr ('TSet t1)
VSet Set (Value t1)
cs)
VPair (Value' Instr l
v1, Value' Instr r
v2) -> do
Value' Instr l
v1' <- DfsSettings m -> Value' Instr l -> m (Value' Instr l)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
settings Value' Instr l
v1
Value' Instr r
v2' <- DfsSettings m -> Value' Instr r -> m (Value' Instr r)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
settings Value' Instr r
v2
Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep (Value t -> m (Value t)) -> Value t -> m (Value t)
forall a b. (a -> b) -> a -> b
$ (Value' Instr l, Value' Instr r) -> Value' Instr ('TPair l r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value' Instr l
v1', Value' Instr r
v2')
VOr 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 t
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 t)
-> (Value' Instr l -> Either (Value' Instr l) (Value' Instr r))
-> Value' Instr l
-> Value t
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 t
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 t)
-> (Value' Instr r -> Either (Value' Instr l) (Value' Instr r))
-> Value' Instr r
-> Value t
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
Map (Value' Instr k) (Value' Instr v) -> Value' Instr ('TMap k v)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(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 v, Comparable k, ForbidBigMap v) =>
Maybe Natural
-> Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
VBigMap Maybe Natural
bmId) Map (Value' Instr k) (Value' Instr v)
vmap
where
recursion1 ::
forall t'.
(Value t' -> Value t)
-> Value t'
-> m (Value t)
recursion1 :: forall (t' :: T). (Value t' -> Value t) -> Value t' -> m (Value t)
recursion1 Value t' -> Value t
constructor Value t'
v = do
Value t'
v' <- DfsSettings m -> Value t' -> m (Value t')
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
settings Value t'
v
Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep (Value t -> m (Value t)) -> Value t -> m (Value t)
forall a b. (a -> b) -> a -> b
$ Value t' -> Value t
constructor Value t'
v'
mapRecursion
:: forall k v. Comparable k
=> (M.Map (Value k) (Value v) -> Value t)
-> M.Map (Value k) (Value v)
-> m (Value t)
mapRecursion :: forall (k :: T) (v :: T).
Comparable k =>
(Map (Value k) (Value v) -> Value t)
-> Map (Value k) (Value v) -> m (Value t)
mapRecursion Map (Value k) (Value v) -> Value t
constructor Map (Value k) (Value v)
vmap = do
Map (Value k) (Value v)
vmap' <-
[(Value k, Value v)] -> Map (Value k) (Value v)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Value k, Value v)] -> Map (Value k) (Value v))
-> m [(Value k, Value v)] -> m (Map (Value k) (Value v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Value k, Value v)]
-> ((Value k, Value v) -> m (Value k, Value v))
-> m [(Value k, Value v)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map (Value k) (Value v) -> [(Value k, Value v)]
forall k a. Map k a -> [(k, a)]
M.toList Map (Value k) (Value v)
vmap) \(Value k
k, Value v
v) -> do
Value k
k' <- DfsSettings m -> Value k -> m (Value k)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
settings Value k
k
Value v
v' <- DfsSettings m -> Value v -> m (Value v)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
settings Value v
v
pure (Value k
k', Value v
v')
Value t -> m (Value t)
forall (t' :: T). Value t' -> m (Value t')
dsValueStep (Value t -> m (Value t)) -> Value t -> m (Value t)
forall a b. (a -> b) -> a -> b
$ Map (Value k) (Value v) -> Value t
constructor Map (Value k) (Value v)
vmap'
dfsFoldMapValue
:: Monoid x
=> (forall t'. Value t' -> x)
-> Value t
-> x
dfsFoldMapValue :: forall x (t :: T).
Monoid x =>
(forall (t' :: T). Value t' -> x) -> Value t -> x
dfsFoldMapValue forall (t' :: T). Value t' -> x
step Value t
v =
Identity x -> x
forall a. Identity a -> a
runIdentity (Identity x -> x) -> Identity x -> x
forall a b. (a -> b) -> a -> b
$ (forall (t' :: T). Value t' -> Identity x) -> Value t -> Identity x
forall x (m :: * -> *) (t :: T).
(Monoid x, Monad m) =>
(forall (t' :: T). Value t' -> m x) -> Value t -> m x
dfsFoldMapValueM (x -> Identity x
forall a. a -> Identity a
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 x (m :: * -> *) (t :: T).
(Monoid x, Monad m) =>
(forall (t' :: T). Value t' -> m x) -> Value t -> m x
dfsFoldMapValueM forall (t' :: T). Value t' -> m x
step Value t
v = do
WriterT x m (Value t) -> m x
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT (WriterT x m (Value t) -> m x) -> WriterT x m (Value t) -> m x
forall a b. (a -> b) -> a -> b
$
DfsSettings (WriterT x m) -> Value t -> WriterT x m (Value t)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue
(DfsSettings (WriterT x m)
forall a. Default a => a
def{ dsValueStep :: forall (t' :: T). Value t' -> WriterT x m (Value t')
dsValueStep =
(\Value t'
val -> do
x
x <- m x -> WriterT x m x
forall (m :: * -> *) a. Monad m => m a -> WriterT x m a
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 :: forall (t :: T). Value t -> Maybe MText
isStringValue =
\case
VString MText
str -> MText -> Maybe MText
forall a. a -> Maybe a
Just MText
str
Value t
_ -> Maybe MText
forall a. Maybe a
Nothing
isBytesValue :: Value t -> Maybe ByteString
isBytesValue :: forall (t :: T). Value t -> Maybe ByteString
isBytesValue =
\case
VBytes ByteString
bytes -> ByteString -> Maybe ByteString
forall a. a -> Maybe a
Just ByteString
bytes
Value t
_ -> Maybe ByteString
forall a. Maybe a
Nothing
allAtomicValues ::
forall t a. (forall t'. Value t' -> Maybe a) -> Value t -> [a]
allAtomicValues :: forall (t :: T) a.
(forall (t' :: T). Value t' -> Maybe a) -> Value t -> [a]
allAtomicValues forall (t' :: T). Value t' -> Maybe a
selector = (forall (t' :: T). Value t' -> [a]) -> Value t -> [a]
forall x (t :: T).
Monoid x =>
(forall (t' :: T). Value t' -> x) -> Value t -> x
dfsFoldMapValue (Maybe a -> [a]
forall a. Maybe a -> [a]
maybeToList (Maybe a -> [a]) -> (Value t' -> Maybe a) -> Value t' -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value t' -> Maybe a
forall (t' :: T). Value t' -> Maybe a
selector)
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 :: forall (t :: T) (s :: [T]).
StorageScope t =>
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 (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value t
v Instr (t : s) (t : s)
forall (inp :: [T]). Instr inp inp
Nop
VOption (Maybe (Value t1)
Nothing :: Maybe (Value tm)) -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope tm) of
Right Dict (ConstantScope t1)
Dict -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage (Value t -> PushableStorageSplit s t)
-> Value t -> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ Maybe (Value t1) -> Value' Instr ('TOption t1)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption Maybe (Value t1)
forall a. Maybe a
Nothing
Left BadTypeForScope
_ -> Instr s (t : s) -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage Instr s (t : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ s, out ~ ('TOption a : s), SingI a) =>
Instr inp out
NONE
VOption (Just Value t1
jVal :: Maybe (Value tm)) -> case Value t1 -> PushableStorageSplit s t1
forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage Value t1
jVal of
ConstantStorage Value t1
_ -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage (Value t -> PushableStorageSplit s t)
-> (Maybe (Value t1) -> Value t)
-> Maybe (Value t1)
-> PushableStorageSplit s t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Value t1) -> Value t
Maybe (Value t1) -> Value' Instr ('TOption t1)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption (Maybe (Value t1) -> PushableStorageSplit s t)
-> Maybe (Value t1) -> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ Value t1 -> Maybe (Value t1)
forall a. a -> Maybe a
Just Value t1
jVal
PushableValueStorage Instr s (t1 : s)
instr -> Instr s (t : s) -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr s (t : s) -> PushableStorageSplit s t)
-> Instr s (t : s) -> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ Instr s (t1 : s)
instr Instr s (t1 : s) -> Instr (t1 : s) (t : s) -> Instr s (t : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (t1 : s) (t : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ ('TOption a : s)) =>
Instr inp out
SOME
PartlyPushableStorage Value heavy
val Instr (heavy : s) (t1 : s)
instr -> Value heavy
-> Instr (heavy : s) (t : s) -> PushableStorageSplit s t
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value heavy
val (Instr (heavy : s) (t : s) -> PushableStorageSplit s t)
-> Instr (heavy : s) (t : s) -> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ Instr (heavy : s) (t1 : s)
instr Instr (heavy : s) (t1 : s)
-> Instr (t1 : s) (t : s) -> Instr (heavy : s) (t : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (t1 : s) (t : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ ('TOption a : s)) =>
Instr inp out
SOME
VList ([Value t1]
vals :: [Value tl]) -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope tl) of
Right Dict (ConstantScope t1)
Dict -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
Left BadTypeForScope
_ ->
let handleList
:: Instr s ('T.TList tl ': s) -> Value tl
-> Maybe (Instr s ('T.TList tl ': s))
handleList :: forall (s :: [T]).
Instr s ('TList t1 : s)
-> Value t1 -> Maybe (Instr s ('TList t1 : s))
handleList Instr s ('TList t1 : s)
instr Value t1
ele = case Value t1 -> PushableStorageSplit ('TList t1 : s) t1
forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage Value t1
ele of
ConstantStorage Value t1
val ->
Instr s ('TList t1 : s) -> Maybe (Instr s ('TList t1 : s))
forall a. a -> Maybe a
Just (Instr s ('TList t1 : s) -> Maybe (Instr s ('TList t1 : s)))
-> Instr s ('TList t1 : s) -> Maybe (Instr s ('TList t1 : s))
forall a b. (a -> b) -> a -> b
$ Instr s ('TList t1 : s)
instr Instr s ('TList t1 : s)
-> Instr ('TList t1 : s) ('TList t1 : s) -> Instr s ('TList t1 : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Value t1 -> Instr ('TList t1 : s) (t1 : 'TList t1 : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value t1
val Instr ('TList t1 : s) (t1 : 'TList t1 : s)
-> Instr (t1 : 'TList t1 : s) ('TList t1 : s)
-> Instr ('TList t1 : s) ('TList t1 : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (t1 : 'TList t1 : s) ('TList t1 : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : 'TList a : s), out ~ ('TList a : s)) =>
Instr inp out
CONS
PushableValueStorage Instr ('TList t1 : s) (t1 : 'TList t1 : s)
eleInstr ->
Instr s ('TList t1 : s) -> Maybe (Instr s ('TList t1 : s))
forall a. a -> Maybe a
Just (Instr s ('TList t1 : s) -> Maybe (Instr s ('TList t1 : s)))
-> Instr s ('TList t1 : s) -> Maybe (Instr s ('TList t1 : s))
forall a b. (a -> b) -> a -> b
$ Instr s ('TList t1 : s)
instr Instr s ('TList t1 : s)
-> Instr ('TList t1 : s) ('TList t1 : s) -> Instr s ('TList t1 : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr ('TList t1 : s) (t1 : 'TList t1 : s)
eleInstr Instr ('TList t1 : s) (t1 : 'TList t1 : s)
-> Instr (t1 : 'TList t1 : s) ('TList t1 : s)
-> Instr ('TList t1 : s) ('TList t1 : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (t1 : 'TList t1 : s) ('TList t1 : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : 'TList a : s), out ~ ('TList a : s)) =>
Instr inp out
CONS
PartlyPushableStorage Value heavy
_ Instr (heavy : 'TList t1 : s) (t1 : 'TList t1 : s)
_ -> Maybe (Instr s ('TList t1 : s))
forall a. Maybe a
Nothing
in PushableStorageSplit s t
-> (Instr s (t : s) -> PushableStorageSplit s t)
-> Maybe (Instr s (t : s))
-> PushableStorageSplit s t
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Value t -> Instr (t : s) (t : s) -> PushableStorageSplit s t
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value t
v Instr (t : s) (t : s)
forall (inp :: [T]). Instr inp inp
Nop) Instr s (t : s) -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Maybe (Instr s (t : s)) -> PushableStorageSplit s t)
-> Maybe (Instr s (t : s)) -> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$
(Instr s (t : s) -> Value t1 -> Maybe (Instr s (t : s)))
-> Instr s (t : s) -> [Value t1] -> Maybe (Instr s (t : s))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Instr s (t : s) -> Value t1 -> Maybe (Instr s (t : s))
Instr s ('TList t1 : s)
-> Value t1 -> Maybe (Instr s ('TList t1 : s))
forall (s :: [T]).
Instr s ('TList t1 : s)
-> Value t1 -> Maybe (Instr s ('TList t1 : s))
handleList Instr s (t : s)
forall {inp :: [T]} {out :: [T]} (p :: T) (s :: [T]).
(inp ~ s, out ~ ('TList p : s), SingI p) =>
Instr inp out
NIL [Value t1]
vals
VSet (Set (Value t1)
_ :: Set (Value t)) -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v ((ForbidOp t1, ForbidNestedBigMaps t1, ForbidTicket t1,
ForbidSaplingState t1, ForbidBigMap t1, ForbidContract t1,
ForbidNonComparable t1) =>
PushableStorageSplit s t)
-> Dict
(ForbidOp t1, ForbidNestedBigMaps t1, ForbidTicket t1,
ForbidSaplingState t1, ForbidBigMap t1, ForbidContract t1,
ForbidNonComparable t1)
-> PushableStorageSplit s t
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Proxy t1
-> Dict
(ForbidOp t1, ForbidNestedBigMaps t1, ForbidTicket t1,
ForbidSaplingState t1, ForbidBigMap t1, ForbidContract t1,
ForbidNonComparable t1)
forall (t :: T) (proxy :: T -> *).
ForbidNonComparable t =>
proxy t -> Dict (ComparabilityImplies t)
comparableImplies (forall {k} (t :: k). Proxy t
forall (t :: T). Proxy t
Proxy @t)
VPair (Value' Instr l
v1 :: Value t1, Value' Instr r
v2 :: Value t2) ->
Value' Instr l
-> (SingI l => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value' Instr l
v1 ((SingI l => PushableStorageSplit s t) -> PushableStorageSplit s t)
-> (SingI l => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ Value' Instr r
-> (SingI r => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value' Instr r
v2 ((SingI r => PushableStorageSplit s t) -> PushableStorageSplit s t)
-> (SingI r => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$
forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @StorageScope @'T.TPair @t1 @t2 (((StorageScope l, StorageScope r) => PushableStorageSplit s t)
-> PushableStorageSplit s t)
-> ((StorageScope l, StorageScope r) => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$
let handlePair
:: PushableStorageSplit s t2
-> PushableStorageSplit (t2 ': s) t1
-> PushableStorageSplit s ('T.TPair t1 t2)
handlePair :: forall (s :: [T]).
PushableStorageSplit s r
-> PushableStorageSplit (r : s) l
-> PushableStorageSplit s ('TPair l r)
handlePair PushableStorageSplit s r
psp2 PushableStorageSplit (r : s) l
psp1 = case (PushableStorageSplit s r
psp2, PushableStorageSplit (r : s) l
psp1) of
(ConstantStorage Value' Instr r
_, ConstantStorage Value' Instr l
_) ->
Value ('TPair l r) -> PushableStorageSplit s ('TPair l r)
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
Value ('TPair l r)
v
(ConstantStorage Value' Instr r
val2, PushableStorageSplit (r : s) l
_) ->
PushableStorageSplit s r
-> PushableStorageSplit (r : s) l
-> PushableStorageSplit s ('TPair l r)
forall (s :: [T]).
PushableStorageSplit s r
-> PushableStorageSplit (r : s) l
-> PushableStorageSplit s ('TPair l r)
handlePair (Instr s (r : s) -> PushableStorageSplit s r
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr s (r : s) -> PushableStorageSplit s r)
-> Instr s (r : s) -> PushableStorageSplit s r
forall a b. (a -> b) -> a -> b
$ Value' Instr r -> Instr s (r : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value' Instr r
val2) PushableStorageSplit (r : s) l
psp1
(PushableStorageSplit s r
_, ConstantStorage Value' Instr l
val1) ->
PushableStorageSplit s r
-> PushableStorageSplit (r : s) l
-> PushableStorageSplit s ('TPair l r)
forall (s :: [T]).
PushableStorageSplit s r
-> PushableStorageSplit (r : s) l
-> PushableStorageSplit s ('TPair l r)
handlePair PushableStorageSplit s r
psp2 (Instr (r : s) (l : r : s) -> PushableStorageSplit (r : s) l
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr (r : s) (l : r : s) -> PushableStorageSplit (r : s) l)
-> Instr (r : s) (l : r : s) -> PushableStorageSplit (r : s) l
forall a b. (a -> b) -> a -> b
$ Value' Instr l -> Instr (r : s) (l : r : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value' Instr l
val1)
(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) ('TPair l r : s) -> Instr s ('TPair l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (r : s) (l : r : s)
instr1 Instr (r : s) (l : r : s)
-> Instr (l : r : s) ('TPair l r : s)
-> Instr (r : s) ('TPair l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (l : r : s) ('TPair l r : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR
(PushableValueStorage Instr s (r : s)
instr2, PartlyPushableStorage Value heavy
val1 Instr (heavy : r : s) (l : r : s)
instr1) ->
Value heavy
-> Instr (heavy : s) ('TPair l r : s)
-> PushableStorageSplit s ('TPair l r)
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value heavy
val1 (Instr (heavy : s) ('TPair l r : s)
-> PushableStorageSplit s ('TPair l r))
-> Instr (heavy : s) ('TPair l r : s)
-> PushableStorageSplit s ('TPair l r)
forall a b. (a -> b) -> a -> b
$ Instr s (r : s) -> Instr (heavy : s) (heavy : r : s)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr s (r : s)
instr2 Instr (heavy : s) (heavy : r : s)
-> Instr (heavy : r : s) ('TPair l r : s)
-> Instr (heavy : s) ('TPair l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (heavy : r : s) (l : r : s)
instr1 Instr (heavy : r : s) (l : r : s)
-> Instr (l : r : s) ('TPair l r : s)
-> Instr (heavy : r : s) ('TPair l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (l : r : s) ('TPair l r : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR
(PartlyPushableStorage Value heavy
val2 Instr (heavy : s) (r : s)
instr2, PushableValueStorage Instr (r : s) (l : r : s)
instr1) ->
Value heavy
-> Instr (heavy : s) ('TPair l r : s)
-> PushableStorageSplit s ('TPair l r)
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value heavy
val2 (Instr (heavy : s) ('TPair l r : s)
-> PushableStorageSplit s ('TPair l r))
-> Instr (heavy : s) ('TPair l r : s)
-> PushableStorageSplit s ('TPair l r)
forall a b. (a -> b) -> a -> b
$ Instr (heavy : s) (r : s)
instr2 Instr (heavy : s) (r : s)
-> Instr (r : s) ('TPair l r : s)
-> Instr (heavy : s) ('TPair l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (r : s) (l : r : s)
instr1 Instr (r : s) (l : r : s)
-> Instr (l : r : s) ('TPair l r : s)
-> Instr (r : s) ('TPair l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (l : r : s) ('TPair l r : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR
(PartlyPushableStorage Value heavy
val2 Instr (heavy : s) (r : s)
instr2, PartlyPushableStorage Value heavy
val1 Instr (heavy : r : s) (l : r : s)
instr1) ->
Value ('TPair heavy heavy)
-> Instr ('TPair heavy heavy : s) ('TPair l r : s)
-> PushableStorageSplit s ('TPair l r)
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage ((Value heavy, Value heavy) -> Value ('TPair heavy heavy)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value heavy
val1, Value heavy
val2)) (Instr ('TPair heavy heavy : s) ('TPair l r : s)
-> PushableStorageSplit s ('TPair l r))
-> Instr ('TPair heavy heavy : s) ('TPair l r : s)
-> PushableStorageSplit s ('TPair l r)
forall a b. (a -> b) -> a -> b
$
Instr ('TPair heavy heavy : s) (heavy : heavy : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : b : s)) =>
Instr inp out
UNPAIR Instr ('TPair heavy heavy : s) (heavy : heavy : s)
-> Instr (heavy : heavy : s) ('TPair l r : s)
-> Instr ('TPair heavy heavy : s) ('TPair l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (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 (heavy : heavy : s) (heavy : r : s)
-> Instr (heavy : r : s) ('TPair l r : s)
-> Instr (heavy : heavy : s) ('TPair l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (heavy : r : s) (l : r : s)
instr1 Instr (heavy : r : s) (l : r : s)
-> Instr (l : r : s) ('TPair l r : s)
-> Instr (heavy : r : s) ('TPair l r : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (l : r : s) ('TPair l r : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR
in PushableStorageSplit s r
-> PushableStorageSplit (r : s) l
-> PushableStorageSplit s ('TPair l r)
forall (s :: [T]).
PushableStorageSplit s r
-> PushableStorageSplit (r : s) l
-> PushableStorageSplit s ('TPair l r)
handlePair (Value' Instr r -> PushableStorageSplit s r
forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage Value' Instr r
v2) (Value' Instr l -> PushableStorageSplit (r : s) l
forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage Value' Instr l
v1)
VOr (Left Value l
orVal :: Either (Value t1) (Value t2)) ->
Value l
-> (SingI l => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value l
orVal ((SingI l => PushableStorageSplit s t) -> PushableStorageSplit s t)
-> (SingI l => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @StorageScope @'T.TOr @t1 @t2 (((StorageScope l, StorageScope r) => PushableStorageSplit s t)
-> PushableStorageSplit s t)
-> ((StorageScope l, StorageScope r) => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$
case Value l -> PushableStorageSplit s l
forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage Value l
orVal of
ConstantStorage Value l
val -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope t2) of
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 (t : s) -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr s (t : s) -> PushableStorageSplit s t)
-> Instr s (t : s) -> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ Value l -> Instr s (l : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value l
val Instr s (l : s) -> Instr (l : s) (t : s) -> Instr s (t : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (l : s) (t : s)
forall {inp :: [T]} {out :: [T]} (b :: T) (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ ('TOr a b : s), SingI b) =>
Instr inp out
LEFT
PushableValueStorage Instr s (l : s)
instr -> Instr s (t : s) -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr s (t : s) -> PushableStorageSplit s t)
-> Instr s (t : s) -> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ Instr s (l : s)
instr Instr s (l : s) -> Instr (l : s) (t : s) -> Instr s (t : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (l : s) (t : s)
forall {inp :: [T]} {out :: [T]} (b :: T) (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ ('TOr a b : s), SingI b) =>
Instr inp out
LEFT
PartlyPushableStorage Value heavy
val Instr (heavy : s) (l : s)
instr -> Value heavy
-> Instr (heavy : s) (t : s) -> PushableStorageSplit s t
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value heavy
val (Instr (heavy : s) (t : s) -> PushableStorageSplit s t)
-> Instr (heavy : s) (t : s) -> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ Instr (heavy : s) (l : s)
instr Instr (heavy : s) (l : s)
-> Instr (l : s) (t : s) -> Instr (heavy : s) (t : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (l : s) (t : s)
forall {inp :: [T]} {out :: [T]} (b :: T) (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ ('TOr a b : s), SingI b) =>
Instr inp out
LEFT
VOr (Right Value r
orVal :: Either (Value t1) (Value t2)) ->
Value r
-> (SingI r => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value r
orVal ((SingI r => PushableStorageSplit s t) -> PushableStorageSplit s t)
-> (SingI r => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @StorageScope @'T.TOr @t1 @t2 (((StorageScope l, StorageScope r) => PushableStorageSplit s t)
-> PushableStorageSplit s t)
-> ((StorageScope l, StorageScope r) => PushableStorageSplit s t)
-> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$
case Value r -> PushableStorageSplit s r
forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage Value r
orVal of
ConstantStorage Value r
val -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope t1) of
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 (t : s) -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr s (t : s) -> PushableStorageSplit s t)
-> Instr s (t : s) -> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ Value r -> Instr s (r : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value r
val Instr s (r : s) -> Instr (r : s) (t : s) -> Instr s (t : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (r : s) (t : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (b : s), out ~ ('TOr a b : s), SingI a) =>
Instr inp out
RIGHT
PushableValueStorage Instr s (r : s)
instr -> Instr s (t : s) -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Instr s (t : s) -> PushableStorageSplit s t)
-> Instr s (t : s) -> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ Instr s (r : s)
instr Instr s (r : s) -> Instr (r : s) (t : s) -> Instr s (t : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (r : s) (t : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (b : s), out ~ ('TOr a b : s), SingI a) =>
Instr inp out
RIGHT
PartlyPushableStorage Value heavy
val Instr (heavy : s) (r : s)
instr -> Value heavy
-> Instr (heavy : s) (t : s) -> PushableStorageSplit s t
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value heavy
val (Instr (heavy : s) (t : s) -> PushableStorageSplit s t)
-> Instr (heavy : s) (t : s) -> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$ Instr (heavy : s) (r : s)
instr Instr (heavy : s) (r : s)
-> Instr (r : s) (t : s) -> Instr (heavy : s) (t : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (r : s) (t : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (b : s), out ~ ('TOr a b : s), SingI a) =>
Instr inp out
RIGHT
VMap (Map (Value k) (Value v)
vMap :: (Map (Value tk) (Value tv))) | Dict (ComparabilityImplies k)
Dict <- Proxy k -> Dict (ComparabilityImplies k)
forall (t :: T) (proxy :: T -> *).
ForbidNonComparable t =>
proxy t -> Dict (ComparabilityImplies t)
comparableImplies (forall {k} (t :: k). Proxy t
forall (t :: T). Proxy t
Proxy @tk) ->
case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope tv) of
Right Dict (ConstantScope v)
Dict -> Value t -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
ConstantScope st =>
Value st -> PushableStorageSplit s st
ConstantStorage Value t
v
Either BadTypeForScope (Dict (ConstantScope v))
_ -> forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @ForbidOp @'T.TMap @tk @tv (((ForbidOp k, ForbidOp v) => PushableStorageSplit s t)
-> PushableStorageSplit s t)
-> ((ForbidOp k, ForbidOp 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 :: forall (s :: [T]).
Instr s ('TMap k v : s)
-> (Value k, Value v) -> Maybe (Instr s ('TMap k v : s))
handleMap Instr s ('TMap k v : s)
instr (Value k
key, Value v
ele) = case Value ('TOption v)
-> PushableStorageSplit ('TMap k v : s) ('TOption v)
forall (t :: T) (s :: [T]).
StorageScope t =>
Value t -> PushableStorageSplit s t
splitPushableStorage (Maybe (Value v) -> Value ('TOption v)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption (Maybe (Value v) -> Value ('TOption v))
-> Maybe (Value v) -> Value ('TOption v)
forall a b. (a -> b) -> a -> b
$ Value v -> Maybe (Value v)
forall a. a -> Maybe a
Just Value v
ele) of
ConstantStorage Value ('TOption v)
val ->
Instr s ('TMap k v : s) -> Maybe (Instr s ('TMap k v : s))
forall a. a -> Maybe a
Just (Instr s ('TMap k v : s) -> Maybe (Instr s ('TMap k v : s)))
-> Instr s ('TMap k v : s) -> Maybe (Instr s ('TMap k v : s))
forall a b. (a -> b) -> a -> b
$ Instr s ('TMap k v : s)
instr Instr s ('TMap k v : s)
-> Instr ('TMap k v : s) ('TMap k v : s) -> Instr s ('TMap k v : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Value ('TOption v)
-> Instr ('TMap k v : s) ('TOption v : 'TMap k v : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value ('TOption v)
val Instr ('TMap k v : s) ('TOption v : 'TMap k v : s)
-> Instr ('TOption v : 'TMap k v : s) ('TMap k v : s)
-> Instr ('TMap k v : s) ('TMap k v : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Value k
-> Instr
('TOption v : 'TMap k v : s) (k : 'TOption v : 'TMap k v : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value k
key Instr ('TOption v : 'TMap k v : s) (k : 'TOption v : 'TMap k v : s)
-> Instr (k : 'TOption v : 'TMap k v : s) ('TMap k v : s)
-> Instr ('TOption v : 'TMap k v : s) ('TMap k v : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (k : 'TOption v : 'TMap k v : s) ('TMap k v : s)
forall {inp :: [T]} {out :: [T]} (c :: T) (s :: [T]).
(inp ~ (UpdOpKey c : UpdOpParams c : c : s), out ~ (c : s),
UpdOp c) =>
Instr inp out
UPDATE
PushableValueStorage Instr ('TMap k v : s) ('TOption v : 'TMap k v : s)
eleInstr ->
Instr s ('TMap k v : s) -> Maybe (Instr s ('TMap k v : s))
forall a. a -> Maybe a
Just (Instr s ('TMap k v : s) -> Maybe (Instr s ('TMap k v : s)))
-> Instr s ('TMap k v : s) -> Maybe (Instr s ('TMap k v : s))
forall a b. (a -> b) -> a -> b
$ Instr s ('TMap k v : s)
instr Instr s ('TMap k v : s)
-> Instr ('TMap k v : s) ('TMap k v : s) -> Instr s ('TMap k v : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr ('TMap k v : s) ('TOption v : 'TMap k v : s)
eleInstr Instr ('TMap k v : s) ('TOption v : 'TMap k v : s)
-> Instr ('TOption v : 'TMap k v : s) ('TMap k v : s)
-> Instr ('TMap k v : s) ('TMap k v : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Value k
-> Instr
('TOption v : 'TMap k v : s) (k : 'TOption v : 'TMap k v : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value k
key Instr ('TOption v : 'TMap k v : s) (k : 'TOption v : 'TMap k v : s)
-> Instr (k : 'TOption v : 'TMap k v : s) ('TMap k v : s)
-> Instr ('TOption v : 'TMap k v : s) ('TMap k v : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (k : 'TOption v : 'TMap k v : s) ('TMap k v : s)
forall {inp :: [T]} {out :: [T]} (c :: T) (s :: [T]).
(inp ~ (UpdOpKey c : UpdOpParams c : c : s), out ~ (c : s),
UpdOp c) =>
Instr inp out
UPDATE
PartlyPushableStorage Value heavy
_ Instr (heavy : 'TMap k v : s) ('TOption v : 'TMap k v : s)
_ -> Maybe (Instr s ('TMap k v : s))
forall a. Maybe a
Nothing
in PushableStorageSplit s t
-> (Instr s (t : s) -> PushableStorageSplit s t)
-> Maybe (Instr s (t : s))
-> PushableStorageSplit s t
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Value t -> Instr (t : s) (t : s) -> PushableStorageSplit s t
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value t
v Instr (t : s) (t : s)
forall (inp :: [T]). Instr inp inp
Nop) Instr s (t : s) -> PushableStorageSplit s t
forall (st :: T) (s :: [T]).
StorageScope st =>
Instr s (st : s) -> PushableStorageSplit s st
PushableValueStorage (Maybe (Instr s (t : s)) -> PushableStorageSplit s t)
-> Maybe (Instr s (t : s)) -> PushableStorageSplit s t
forall a b. (a -> b) -> a -> b
$
(Instr s (t : s) -> (Value k, Value v) -> Maybe (Instr s (t : s)))
-> Instr s (t : s)
-> [(Value k, Value v)]
-> Maybe (Instr s (t : s))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Instr s (t : s) -> (Value k, Value v) -> Maybe (Instr s (t : s))
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 (t : s)
forall {inp :: [T]} {out :: [T]} (b :: T) (a :: T) (s :: [T]).
(inp ~ s, out ~ ('TMap a b : s), SingI b, Comparable a) =>
Instr inp out
EMPTY_MAP ([(Value k, Value v)] -> Maybe (Instr s (t : s)))
-> [(Value k, Value v)] -> Maybe (Instr s (t : s))
forall a b. (a -> b) -> a -> b
$ Map (Value k) (Value v) -> [(Value k, Value v)]
forall k a. Map k a -> [(k, a)]
M.toList Map (Value k) (Value v)
vMap
VBigMap Maybe Natural
_ Map (Value' Instr k) (Value' Instr v)
_ -> Value t -> Instr (t : s) (t : s) -> PushableStorageSplit s t
forall (xs :: T) (st :: T) (s :: [T]).
(StorageScope xs, StorageScope st) =>
Value xs -> Instr (xs : s) (st : s) -> PushableStorageSplit s st
PartlyPushableStorage Value t
v Instr (t : s) (t : s)
forall (inp :: [T]). Instr inp inp
Nop
isMichelsonInstr :: Instr i o -> Bool
isMichelsonInstr :: forall (i :: [T]) (o :: [T]). Instr i o -> Bool
isMichelsonInstr = (forall (cls :: InstrClass).
(SingI cls, WCIConstraint Instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls i o -> Bool)
-> Instr i o -> Bool
forall t (inp :: [T]) (out :: [T]) r.
ClassifyInstr t =>
(forall (cls :: InstrClass).
(SingI cls, WCIConstraint Instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r)
-> Instr inp out -> r
forall (instr :: [T] -> [T] -> *) t (inp :: [T]) (out :: [T]) r.
(WithClassifiedInstr instr, ClassifyInstr t) =>
(forall (cls :: InstrClass).
(SingI cls, WCIConstraint instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r)
-> instr inp out -> r
withClassifiedInstr ((forall (cls :: InstrClass).
(SingI cls, WCIConstraint Instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls i o -> Bool)
-> Instr i o -> Bool)
-> (forall (cls :: InstrClass).
(SingI cls, WCIConstraint Instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls i o -> Bool)
-> Instr i o
-> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> ClassifiedInstr cls i o -> Bool
forall a b. a -> b -> a
const (Bool -> ClassifiedInstr cls i o -> Bool)
-> (SingIsMichelson (GetClassified cls) -> Bool)
-> SingIsMichelson (GetClassified cls)
-> ClassifiedInstr cls i o
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
SingIsMichelson (GetClassified cls)
SFromMichelson -> Bool
True
SingIsMichelson (GetClassified cls)
SStructural -> Bool
True
SingIsMichelson (GetClassified cls)
SAdditional -> Bool
False
SingIsMichelson (GetClassified cls)
SPhantom -> Bool
False
data SomeAnns where
SomeAnns :: Anns xs -> SomeAnns
SomeUncheckedAnns :: NonEmpty AnyAnn -> SomeAnns
instrAnns :: Instr i o -> Maybe SomeAnns
instrAnns :: forall (i :: [T]) (o :: [T]). Instr i o -> Maybe SomeAnns
instrAnns = (forall (cls :: InstrClass).
(SingI cls, WCIConstraint Instr cls) =>
Sing (GetClassified cls)
-> ClassifiedInstr cls i o -> Maybe SomeAnns)
-> Instr i o -> Maybe SomeAnns
forall t (inp :: [T]) (out :: [T]) r.
ClassifyInstr t =>
(forall (cls :: InstrClass).
(SingI cls, WCIConstraint Instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r)
-> Instr inp out -> r
forall (instr :: [T] -> [T] -> *) t (inp :: [T]) (out :: [T]) r.
(WithClassifiedInstr instr, ClassifyInstr t) =>
(forall (cls :: InstrClass).
(SingI cls, WCIConstraint instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r)
-> instr inp out -> r
withClassifiedInstr \case
Sing (GetClassified cls)
SingHasAnns (GetClassified cls)
SDoesNotHaveAnns -> Maybe SomeAnns -> ClassifiedInstr cls i o -> Maybe SomeAnns
forall a b. a -> b -> a
const Maybe SomeAnns
forall a. Maybe a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
Sing (GetClassified cls)
SingHasAnns (GetClassified cls)
SDoesHaveStandardAnns -> $(do
TH.TyConI (TH.DataD _ _ _ _ cons _) <- TH.reify ''ClassifiedInstr
let mkMatch = \case
TH.ForallC _ _ con -> mkMatch con
TH.GadtC [nm] tys res
| null $ listify (== 'DoesHaveStandardAnns) res
-> Nothing
| otherwise
-> Just $ TH.match
(TH.conP nm ([p|anns|] : replicate (length $ drop 1 tys) TH.wildP))
(TH.normalB [|pure $ SomeAnns anns|]) []
x -> error $ "Unexpected constructor " <> show (TH.ppr x)
TH.lamCaseE $ mapMaybe mkMatch cons
)
Sing (GetClassified cls)
SingHasAnns (GetClassified cls)
SDoesHaveNonStandardAnns -> \case
C_AnnMIN_BLOCK_TIME [AnyAnn]
anns -> NonEmpty AnyAnn -> SomeAnns
SomeUncheckedAnns (NonEmpty AnyAnn -> SomeAnns)
-> Maybe (NonEmpty AnyAnn) -> Maybe SomeAnns
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [AnyAnn] -> Maybe (NonEmpty AnyAnn)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [AnyAnn]
anns
C_AnnEMIT AnnVar
anns' FieldAnn
tag Maybe (Notes t)
ty ->
SomeAnns -> Maybe SomeAnns
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnns -> Maybe SomeAnns) -> SomeAnns -> Maybe SomeAnns
forall a b. (a -> b) -> a -> b
$ case Maybe (Notes t)
ty of
Just Notes t
ty' -> Anns '[FieldAnn, Notes t, VarAnn] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns (Anns '[FieldAnn, Notes t, VarAnn] -> SomeAnns)
-> Anns '[FieldAnn, Notes t, VarAnn] -> SomeAnns
forall a b. (a -> b) -> a -> b
$ FieldAnn
tag FieldAnn
-> Anns '[Notes t, VarAnn] -> Anns '[FieldAnn, Notes t, VarAnn]
forall {k} (tag :: k) (xs1 :: [*]).
Typeable tag =>
Annotation tag -> Anns xs1 -> Anns (Annotation tag : xs1)
`AnnsCons` Notes t
ty' Notes t -> AnnVar -> Anns '[Notes t, VarAnn]
forall (t :: T) (xs1 :: [*]).
SingI t =>
Notes t -> Anns xs1 -> Anns (Notes t : xs1)
`AnnsTyCons` AnnVar
anns'
Maybe (Notes t)
Nothing -> Anns '[FieldAnn, VarAnn] -> SomeAnns
forall (xs :: [*]). Anns xs -> SomeAnns
SomeAnns (Anns '[FieldAnn, VarAnn] -> SomeAnns)
-> Anns '[FieldAnn, VarAnn] -> SomeAnns
forall a b. (a -> b) -> a -> b
$ FieldAnn
tag FieldAnn -> AnnVar -> Anns '[FieldAnn, VarAnn]
forall {k} (tag :: k) (xs1 :: [*]).
Typeable tag =>
Annotation tag -> Anns xs1 -> Anns (Annotation tag : xs1)
`AnnsCons` AnnVar
anns'