{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
module Morley.Michelson.Optimizer
( optimize
, optimizeWithConf
, defaultOptimizerConf
, defaultRules
, defaultRulesAndPushPack
, orRule
, orSimpleRule
, Rule (..)
, OptimizerConf (..)
, ocGotoValuesL
) where
import Prelude hiding (EQ, GT, LT)
import Control.Lens (makeLensesFor)
import Data.Constraint (Dict(..))
import Data.Default (Default(def))
import Data.Singletons (sing)
import Data.Type.Equality ((:~:)(Refl))
import Morley.Michelson.Interpret.Pack (packValue')
import Morley.Michelson.Typed.Aliases (Value)
import Morley.Michelson.Typed.Arith
import Morley.Michelson.Typed.Instr
import Morley.Michelson.Typed.Scope (ConstantScope, PackedValScope, checkScope)
import Morley.Michelson.Typed.Sing
import Morley.Michelson.Typed.T
import Morley.Michelson.Typed.Util (DfsSettings(..), dfsModifyInstr)
import Morley.Michelson.Typed.Value
import Morley.Util.PeanoNatural
data OptimizerConf = OptimizerConf
{ OptimizerConf -> Bool
ocGotoValues :: Bool
, OptimizerConf -> [Rule]
ocRuleset :: [Rule]
}
defaultOptimizerConf :: OptimizerConf
defaultOptimizerConf :: OptimizerConf
defaultOptimizerConf = OptimizerConf :: Bool -> [Rule] -> OptimizerConf
OptimizerConf
{ ocGotoValues :: Bool
ocGotoValues = Bool
True
, ocRuleset :: [Rule]
ocRuleset = [Rule]
defaultRules
}
instance Default OptimizerConf where
def :: OptimizerConf
def = OptimizerConf
defaultOptimizerConf
optimize :: Instr inp out -> Instr inp out
optimize :: forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
optimize = OptimizerConf -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
OptimizerConf -> Instr inp out -> Instr inp out
optimizeWithConf OptimizerConf
forall a. Default a => a
def
optimizeWithConf :: OptimizerConf -> Instr inp out -> Instr inp out
optimizeWithConf :: forall (inp :: [T]) (out :: [T]).
OptimizerConf -> Instr inp out -> Instr inp out
optimizeWithConf (OptimizerConf Bool
ocGotoValues [Rule]
rules) Instr inp out
instr = (Instr inp out -> Element [Rule] -> Instr inp out)
-> Instr inp out -> [Rule] -> Instr inp out
forall t b. Container t => (b -> Element t -> b) -> b -> t -> b
foldl ((Rule -> Instr inp out -> Instr inp out)
-> Instr inp out -> Rule -> Instr inp out
forall a b c. (a -> b -> c) -> b -> a -> c
flip Rule -> Instr inp out -> Instr inp out
performOneStage) Instr inp out
instrRHS [Rule]
rules
where
dfsSettings :: DfsSettings Identity
dfsSettings = DfsSettings Identity
forall a. Default a => a
def{ dsGoToValues :: Bool
dsGoToValues = Bool
ocGotoValues }
performOneStage :: Rule -> Instr inp out -> Instr inp out
performOneStage Rule
stageRules =
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
dfsSettings ((forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out)
-> Instr inp out -> Instr inp out)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
forall a b. (a -> b) -> a -> b
$ Rule -> Instr i o -> Instr i o
forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
applyOnce Rule
stageRules
instrRHS :: Instr inp out
instrRHS = Rule -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
applyOnce ((Rule -> Rule) -> Rule
fixpoint Rule -> Rule
flattenSeqLHS) Instr inp out
instr
newtype Rule = Rule {Rule
-> forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
unRule :: forall inp out. Instr inp out -> Maybe (Instr inp out)}
defaultRules :: [Rule]
defaultRules :: [Rule]
defaultRules = ((Rule -> Rule) -> Rule) -> [Rule -> Rule] -> [Rule]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map (Rule -> Rule) -> Rule
fixpoint
[ Rule -> Rule
mainStageRules
, Rule -> Rule
glueAdjacentDropsStageRules
]
where
glueAdjacentDropsStageRules :: Rule -> Rule
glueAdjacentDropsStageRules = Rule -> Rule
flattenSeqLHS (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
adjacentDrops
defaultRulesAndPushPack :: [Rule]
defaultRulesAndPushPack :: [Rule]
defaultRulesAndPushPack =
case [Rule]
defaultRules of
Rule
_ : [Rule]
otherStagesRules -> do
let mainStageRulesAndPushPack :: Rule
mainStageRulesAndPushPack = (Rule -> Rule) -> Rule
fixpoint ((Rule -> Rule) -> Rule) -> (Rule -> Rule) -> Rule
forall a b. (a -> b) -> a -> b
$ Rule -> Rule
mainStageRules (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
pushPack
Rule
mainStageRulesAndPushPack Rule -> [Rule] -> [Rule]
forall a. a -> [a] -> [a]
: [Rule]
otherStagesRules
[Rule]
_ -> Text -> [Rule]
forall a. HasCallStack => Text -> a
error Text
"`defaultRules` should not be empty"
mainStageRules :: Rule -> Rule
mainStageRules :: Rule -> Rule
mainStageRules =
Rule -> Rule
flattenSeqLHS
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
removeNesting
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
removeExtStackType
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
dipDrop2swapDrop
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
ifNopNop2Drop
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
nopIsNeutralForSeq
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
variousNops
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
dupSwap2dup
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
noDipNeeded
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
branchShortCut
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
compareWithZero
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
simpleDrops
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
internalNop
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
simpleDips
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
simpleDups
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
adjacentDips
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
isSomeOnIf
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
redundantIf
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
emptyDip
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
digDug
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
specificPush
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
pairUnpair
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
pairMisc
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
unpairMisc
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
swapBeforeCommutative
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
justDrops
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
justDoubleDrops
flattenSeqLHS :: Rule -> Rule
flattenSeqLHS :: Rule -> Rule
flattenSeqLHS Rule
toplevel = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
it :: Instr inp out
it@(Seq (Seq Instr inp b
_ Instr b b
_) Instr b out
_) -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Rule -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
linearizeAndReapply Rule
toplevel Instr inp out
it
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
removeNesting :: Rule
removeNesting :: Rule
removeNesting = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
Nested Instr inp out
i -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
i
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
removeExtStackType :: Rule
removeExtStackType :: Rule
removeExtStackType = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
Ext (STACKTYPE{}) -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
dipDrop2swapDrop :: Rule
dipDrop2swapDrop :: Rule
dipDrop2swapDrop = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
DIP Instr a c
DROP -> Instr (b : a : c) (b : c) -> Maybe (Instr (b : a : c) (b : c))
forall a. a -> Maybe a
Just (Instr (b : a : c) (b : c) -> Maybe (Instr (b : a : c) (b : c)))
-> Instr (b : a : c) (b : c) -> Maybe (Instr (b : a : c) (b : c))
forall a b. (a -> b) -> a -> b
$ Instr (b : a : c) (a : b : c)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP Instr (b : a : c) (a : b : c)
-> Instr (a : b : c) (b : c) -> Instr (b : a : c) (b : c)
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : b : c) (b : c)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
ifNopNop2Drop :: Rule
ifNopNop2Drop :: Rule
ifNopNop2Drop = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
IF Instr s out
Nop Instr s out
Nop -> Instr ('TBool : out) out -> Maybe (Instr ('TBool : out) out)
forall a. a -> Maybe a
Just Instr ('TBool : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
nopIsNeutralForSeq :: Rule
nopIsNeutralForSeq :: Rule
nopIsNeutralForSeq = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
Instr inp b
Nop :# Instr b out
i -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
i
Instr inp b
i :# Instr b out
Nop -> Instr inp b -> Maybe (Instr inp b)
forall a. a -> Maybe a
Just Instr inp b
i
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
variousNops :: Rule
variousNops :: Rule
variousNops = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
Instr inp b
DUP :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
DUPN PeanoNatural n
_ :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
SWAP :# Instr b b
SWAP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
PUSH Value' Instr t
_ :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
NONE :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
UNIT :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
NIL :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
EMPTY_SET :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
EMPTY_MAP :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
EMPTY_BIG_MAP :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
LAMBDA IsNotInView => RemFail Instr '[i] '[o]
_ :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
SELF SomeEntrypointCallT arg
_ :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
NOW :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
AMOUNT :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
BALANCE :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
TOTAL_VOTING_POWER :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
SOURCE :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
SENDER :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
CHAIN_ID :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
LEVEL :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
SELF_ADDRESS :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
READ_TICKET :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
DUP :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
DUPN PeanoNatural n
_ :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
SWAP :# Instr b out
SWAP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
PUSH Value' Instr t
_ :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
NONE :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
UNIT :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
NIL :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
EMPTY_SET :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
EMPTY_MAP :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
EMPTY_BIG_MAP :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
LAMBDA IsNotInView => RemFail Instr '[i] '[o]
_ :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
SELF SomeEntrypointCallT arg
_ :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
NOW :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
AMOUNT :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
BALANCE :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
TOTAL_VOTING_POWER :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
SOURCE :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
SENDER :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
CHAIN_ID :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
LEVEL :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
SELF_ADDRESS :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
READ_TICKET :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
dupSwap2dup :: Rule
dupSwap2dup :: Rule
dupSwap2dup = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
Instr inp b
DUP :# Instr b b
SWAP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp b
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ (a : a : s), DupableScope a) =>
Instr inp out
DUP Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
Instr inp b
DUP :# Instr b out
SWAP -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ (a : a : s), DupableScope a) =>
Instr inp out
DUP
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
noDipNeeded :: Rule
noDipNeeded :: Rule
noDipNeeded = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
PUSH Value' Instr t
x :# DIP Instr a c
f :# Instr b out
c -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Value' Instr t -> Instr c b
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 t
x Instr c b -> Instr b out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
PUSH Value' Instr t
x :# DIP Instr a c
f -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Value' Instr t -> Instr c out
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 t
x
Instr inp b
UNIT :# DIP Instr a c
f :# Instr b out
c -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c b
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TUnit : s)) =>
Instr inp out
UNIT Instr c b -> Instr b out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
UNIT :# DIP Instr a c
f -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c out
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TUnit : s)) =>
Instr inp out
UNIT
Instr inp b
NOW :# DIP Instr a c
f :# Instr b out
c -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c b
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TTimestamp : s)) =>
Instr inp out
NOW Instr c b -> Instr b out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
NOW :# DIP Instr a c
f -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c out
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TTimestamp : s)) =>
Instr inp out
NOW
Instr inp b
SENDER :# DIP Instr a c
f :# Instr b out
c -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c b
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TAddress : s)) =>
Instr inp out
SENDER Instr c b -> Instr b out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
SENDER :# DIP Instr a c
f -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c out
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TAddress : s)) =>
Instr inp out
SENDER
Instr inp b
EMPTY_MAP :# DIP Instr a c
f :# Instr b out
c -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c b
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ s, out ~ ('TMap a b : s), SingI a, SingI b, Comparable a) =>
Instr inp out
EMPTY_MAP Instr c b -> Instr b out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
EMPTY_MAP :# DIP Instr a c
f -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c out
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ s, out ~ ('TMap a b : s), SingI a, SingI b, Comparable a) =>
Instr inp out
EMPTY_MAP
Instr inp b
EMPTY_SET :# DIP Instr a c
f :# Instr b out
c -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c b
forall {inp :: [T]} {out :: [T]} (e :: T) (s :: [T]).
(inp ~ s, out ~ ('TSet e : s), SingI e, Comparable e) =>
Instr inp out
EMPTY_SET Instr c b -> Instr b out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
EMPTY_SET :# DIP Instr a c
f -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c out
forall {inp :: [T]} {out :: [T]} (e :: T) (s :: [T]).
(inp ~ s, out ~ ('TSet e : s), SingI e, Comparable e) =>
Instr inp out
EMPTY_SET
DIP Instr a c
f :# Instr b b
DROP :# Instr b out
c -> Instr (b : a) out -> Maybe (Instr (b : a) out)
forall a. a -> Maybe a
Just (Instr (b : a) out -> Maybe (Instr (b : a) out))
-> Instr (b : a) out -> Maybe (Instr (b : a) out)
forall a b. (a -> b) -> a -> b
$ Instr (b : a) a
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (b : a) a -> Instr a out -> Instr (b : a) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c out
Instr b out
c
DIP Instr a c
f :# Instr b out
DROP -> Instr (b : a) c -> Maybe (Instr (b : a) c)
forall a. a -> Maybe a
Just (Instr (b : a) c -> Maybe (Instr (b : a) c))
-> Instr (b : a) c -> Maybe (Instr (b : a) c)
forall a b. (a -> b) -> a -> b
$ Instr (b : a) a
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (b : a) a -> Instr a c -> Instr (b : a) c
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr a c
f
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
branchShortCut :: Rule
branchShortCut :: Rule
branchShortCut = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
Instr inp b
LEFT :# IF_LEFT Instr (a : s) b
f Instr (b : s) b
_ :# Instr b out
c -> Instr (a : s) out -> Maybe (Instr (a : s) out)
forall a. a -> Maybe a
Just (Instr (a : s) b
f Instr (a : s) b -> Instr b out -> Instr (a : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
Instr inp b
RIGHT :# IF_LEFT Instr (a : s) b
_ Instr (b : s) b
f :# Instr b out
c -> Instr (b : s) out -> Maybe (Instr (b : s) out)
forall a. a -> Maybe a
Just (Instr (b : s) b
f Instr (b : s) b -> Instr b out -> Instr (b : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
Instr inp b
CONS :# IF_CONS Instr (a : 'TList a : s) b
f Instr s b
_ :# Instr b out
c -> Instr (a : 'TList a : s) out
-> Maybe (Instr (a : 'TList a : s) out)
forall a. a -> Maybe a
Just (Instr (a : 'TList a : s) b
f Instr (a : 'TList a : s) b
-> Instr b out -> Instr (a : 'TList a : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
Instr inp b
NIL :# IF_CONS Instr (a : 'TList a : s) b
_ Instr s b
f :# Instr b out
c -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Instr s b
f Instr s b -> Instr b out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
Instr inp b
NONE :# IF_NONE Instr s b
f Instr (a : s) b
_ :# Instr b out
c -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Instr s b
f Instr s b -> Instr b out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
Instr inp b
SOME :# IF_NONE Instr s b
_ Instr (a : s) b
f :# Instr b out
c -> Instr (a : s) out -> Maybe (Instr (a : s) out)
forall a. a -> Maybe a
Just (Instr (a : s) b
f Instr (a : s) b -> Instr b out -> Instr (a : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
PUSH vOr :: Value' Instr t
vOr@(VOr Either (Value' Instr l) (Value' Instr r)
eitherVal) :# IF_LEFT Instr (a : s) b
f Instr (b : s) b
g :# Instr b out
c -> case Value' Instr t
vOr of
(Value ('TOr l r)
_ :: Value ('TOr l r)) -> case Either (Value' Instr l) (Value' Instr r)
eitherVal of
Left Value' Instr l
val -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope l) of
Right Dict (ConstantScope l)
Dict -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr l -> Instr inp (a : 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
val Instr inp (a : s) -> Instr (a : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : s) b
f Instr (a : s) b -> Instr b out -> Instr (a : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
Either BadTypeForScope (Dict (ConstantScope l))
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
Right Value' Instr r
val -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope r) of
Right Dict (ConstantScope r)
Dict -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr r -> Instr inp (b : 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
val Instr inp (b : s) -> Instr (b : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (b : s) b
g Instr (b : s) b -> Instr b out -> Instr (b : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
Either BadTypeForScope (Dict (ConstantScope r))
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
PUSH (VList (Value' Instr t1
x : [Value' Instr t1]
xs)) :# IF_CONS Instr (a : 'TList a : s) b
f Instr s b
_ :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr ('TList t1) -> Instr inp ('TList t1 : inp)
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 t1] -> Value' Instr ('TList t1)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
VList [Value' Instr t1]
xs) Instr inp ('TList t1 : inp)
-> Instr ('TList t1 : inp) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Value' Instr t1 -> Instr ('TList t1 : inp) (a : 'TList a : 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 t1
x Instr ('TList t1 : inp) (a : 'TList a : s)
-> Instr (a : 'TList a : s) out -> Instr ('TList t1 : inp) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : 'TList a : s) b
f Instr (a : 'TList a : s) b
-> Instr b out -> Instr (a : 'TList a : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
PUSH (VList [Value' Instr t1]
_) :# IF_CONS Instr (a : 'TList a : s) b
_ Instr s b
f :# Instr b out
c -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Instr s b
f Instr s b -> Instr b out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
PUSH (VOption Maybe (Value' Instr t1)
Nothing) :# IF_NONE Instr s b
f Instr (a : s) b
_ :# Instr b out
c -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Instr s b
f Instr s b -> Instr b out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
PUSH (VOption (Just Value' Instr t1
val)) :# IF_NONE Instr s b
_ Instr (a : s) b
f :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr t1 -> Instr inp (a : 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 t1
val Instr inp (a : s) -> Instr (a : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : s) b
f Instr (a : s) b -> Instr b out -> Instr (a : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
PUSH (VBool Bool
True) :# IF Instr s b
f Instr s b
_ :# Instr b out
c -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Instr s b
f Instr s b -> Instr b out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
PUSH (VBool Bool
False) :# IF Instr s b
_ Instr s b
f :# Instr b out
c -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Instr s b
f Instr s b -> Instr b out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
Instr inp b
LEFT :# IF_LEFT Instr (a : s) out
f Instr (b : s) out
_ -> Instr (a : s) out -> Maybe (Instr (a : s) out)
forall a. a -> Maybe a
Just Instr (a : s) out
f
Instr inp b
RIGHT :# IF_LEFT Instr (a : s) out
_ Instr (b : s) out
f -> Instr (b : s) out -> Maybe (Instr (b : s) out)
forall a. a -> Maybe a
Just Instr (b : s) out
f
Instr inp b
CONS :# IF_CONS Instr (a : 'TList a : s) out
f Instr s out
_ -> Instr (a : 'TList a : s) out
-> Maybe (Instr (a : 'TList a : s) out)
forall a. a -> Maybe a
Just Instr (a : 'TList a : s) out
f
Instr inp b
NIL :# IF_CONS Instr (a : 'TList a : s) out
_ Instr s out
f -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just Instr s out
f
Instr inp b
NONE :# IF_NONE Instr s out
f Instr (a : s) out
_ -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just Instr s out
f
Instr inp b
SOME :# IF_NONE Instr s out
_ Instr (a : s) out
f -> Instr (a : s) out -> Maybe (Instr (a : s) out)
forall a. a -> Maybe a
Just Instr (a : s) out
f
PUSH vOr :: Value' Instr t
vOr@(VOr Either (Value' Instr l) (Value' Instr r)
eitherVal) :# IF_LEFT Instr (a : s) out
f Instr (b : s) out
g -> case Value' Instr t
vOr of
(Value ('TOr l r)
_ :: Value ('TOr l r)) -> case Either (Value' Instr l) (Value' Instr r)
eitherVal of
Left Value' Instr l
val -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope l) of
Right Dict (ConstantScope l)
Dict -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr l -> Instr inp (a : 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
val Instr inp (a : s) -> Instr (a : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : s) out
f)
Either BadTypeForScope (Dict (ConstantScope l))
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
Right Value' Instr r
val -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope r) of
Right Dict (ConstantScope r)
Dict -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr r -> Instr inp (b : 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
val Instr inp (b : s) -> Instr (b : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (b : s) out
g)
Either BadTypeForScope (Dict (ConstantScope r))
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
PUSH (VList (Value' Instr t1
x : [Value' Instr t1]
xs)) :# IF_CONS Instr (a : 'TList a : s) out
f Instr s out
_ -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr ('TList t1) -> Instr inp ('TList t1 : inp)
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 t1] -> Value' Instr ('TList t1)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
VList [Value' Instr t1]
xs) Instr inp ('TList t1 : inp)
-> Instr ('TList t1 : inp) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Value' Instr t1 -> Instr ('TList t1 : inp) (a : 'TList a : 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 t1
x Instr ('TList t1 : inp) (a : 'TList a : s)
-> Instr (a : 'TList a : s) out -> Instr ('TList t1 : inp) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : 'TList a : s) out
f)
PUSH (VList [Value' Instr t1]
_) :# IF_CONS Instr (a : 'TList a : s) out
_ Instr s out
f -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just Instr s out
f
PUSH (VOption Maybe (Value' Instr t1)
Nothing) :# IF_NONE Instr s out
f Instr (a : s) out
_ -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just Instr s out
f
PUSH (VOption (Just Value' Instr t1
val)) :# IF_NONE Instr s out
_ Instr (a : s) out
f -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr t1 -> Instr inp (a : 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 t1
val Instr inp (a : s) -> Instr (a : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : s) out
f)
PUSH (VBool Bool
True) :# IF Instr s out
f Instr s out
_ -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just Instr s out
f
PUSH (VBool Bool
False) :# IF Instr s out
_ Instr s out
f -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just Instr s out
f
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
compareWithZero :: Rule
compareWithZero :: Rule
compareWithZero = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
PUSH (VInt Integer
0) :# Instr b b
COMPARE :# Instr b b
EQ :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp b
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Eq' n : s),
UnaryArithOp Eq' n) =>
Instr inp out
EQ Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
PUSH (VNat Natural
0) :# Instr b b
COMPARE :# Instr b b
EQ :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp ('TInt : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ ('TInt : s), ToIntArithOp n) =>
Instr inp out
INT Instr inp ('TInt : s) -> Instr ('TInt : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TInt : s) b
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Eq' n : s),
UnaryArithOp Eq' n) =>
Instr inp out
EQ Instr ('TInt : s) b -> Instr b out -> Instr ('TInt : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
PUSH (VInt Integer
0) :# Instr b b
COMPARE :# Instr b out
EQ -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Eq' n : s),
UnaryArithOp Eq' n) =>
Instr inp out
EQ
PUSH (VNat Natural
0) :# Instr b b
COMPARE :# Instr b out
EQ -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp ('TInt : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ ('TInt : s), ToIntArithOp n) =>
Instr inp out
INT Instr inp ('TInt : s) -> Instr ('TInt : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TInt : s) out
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Eq' n : s),
UnaryArithOp Eq' n) =>
Instr inp out
EQ
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
simpleDrops :: Rule
simpleDrops :: Rule
simpleDrops = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
DROPN PeanoNatural n
Zero :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
DROPN PeanoNatural n
Zero -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
internalNop :: Rule
internalNop :: Rule
internalNop = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
DIP Instr a c
Nop -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
DIP Instr a c
Nop :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
simpleDips :: Rule
simpleDips :: Rule
simpleDips = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
DIPN PeanoNatural n
Zero Instr s s'
i :# Instr b out
c -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Instr s s'
i Instr s s' -> Instr s' out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr s' out
c)
DIPN PeanoNatural n
Zero Instr s s'
i -> Instr s s' -> Maybe (Instr s s')
forall a. a -> Maybe a
Just Instr s s'
i
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
simpleDups :: Rule
simpleDups :: Rule
simpleDups = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
DUPN PeanoNatural n
One :# Instr b out
xs -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp b
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ (a : a : s), DupableScope a) =>
Instr inp out
DUP Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
xs
DUPN PeanoNatural n
One -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ (a : a : s), DupableScope a) =>
Instr inp out
DUP
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
adjacentDips :: Rule
adjacentDips :: Rule
adjacentDips = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
DIP Instr a c
f :# DIP Instr a c
g -> Instr (b : a) (b : c) -> Maybe (Instr (b : a) (b : c))
forall a. a -> Maybe a
Just (Instr a c -> Instr (b : a) (b : c)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP (Instr a c
f Instr a c -> Instr c c -> Instr a c
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c c
Instr a c
g))
DIP Instr a c
f :# DIP Instr a c
g :# Instr b out
c -> Instr (b : a) out -> Maybe (Instr (b : a) out)
forall a. a -> Maybe a
Just (Instr a c -> Instr (b : a) (b : c)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP (Instr a c
f Instr a c -> Instr c c -> Instr a c
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c c
Instr a c
g) Instr (b : a) (b : c) -> Instr (b : c) out -> Instr (b : a) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr (b : c) out
c)
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
redundantIf :: Rule
redundantIf :: Rule
redundantIf = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule \case
IF Instr s b
x Instr s b
y :# Instr b out
xs
| Instr s b
x Instr s b -> Instr s b -> Bool
forall a. Eq a => a -> a -> Bool
== Instr s b
y
-> Instr ('TBool : s) out -> Maybe (Instr ('TBool : s) out)
forall a. a -> Maybe a
Just (Instr ('TBool : s) out -> Maybe (Instr ('TBool : s) out))
-> Instr ('TBool : s) out -> Maybe (Instr ('TBool : s) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TBool : s) s
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TBool : s) s -> Instr s out -> Instr ('TBool : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr s b
x Instr s b -> Instr b out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
xs
IF Instr s out
x Instr s out
y
| Instr s out
x Instr s out -> Instr s out -> Bool
forall a. Eq a => a -> a -> Bool
== Instr s out
y
-> Instr ('TBool : s) out -> Maybe (Instr ('TBool : s) out)
forall a. a -> Maybe a
Just (Instr ('TBool : s) out -> Maybe (Instr ('TBool : s) out))
-> Instr ('TBool : s) out -> Maybe (Instr ('TBool : s) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TBool : s) s
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TBool : s) s -> Instr s out -> Instr ('TBool : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr s out
x
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
emptyDip :: Rule
emptyDip :: Rule
emptyDip = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule \case
DIP Instr a c
Nop :# Instr b out
xs -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
xs
DIP Instr a c
Nop -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
DIPN PeanoNatural n
_ Instr s s'
Nop :# Instr b out
xs -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
xs
DIPN PeanoNatural n
_ Instr s s'
Nop -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
digDug :: Rule
digDug :: Rule
digDug = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule \case
(DIG (PeanoNatural n
x :: PeanoNatural n) :: Instr inp t) :# (DUG PeanoNatural n
y :: Instr t out) :# Instr b out
xs
| Just n :~: n
Refl <- PeanoNatural n -> PeanoNatural n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat).
PeanoNatural a -> PeanoNatural b -> Maybe (a :~: b)
eqPeanoNat PeanoNatural n
x PeanoNatural n
y
-> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
xs
(DIG (PeanoNatural n
x :: PeanoNatural n) :: Instr inp t) :# (DUG PeanoNatural n
y :: Instr t out)
| Just n :~: n
Refl <- PeanoNatural n -> PeanoNatural n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat).
PeanoNatural a -> PeanoNatural b -> Maybe (a :~: b)
eqPeanoNat PeanoNatural n
x PeanoNatural n
y
-> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
adjacentDrops :: Rule
adjacentDrops :: Rule
adjacentDrops = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
Instr inp b
DROP :# Instr b out
DROP -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (PeanoNatural ('S ('S 'Z))
-> Instr (a : a : out) (Drop ('S ('S 'Z)) (a : a : out))
forall (n :: Nat) (inp :: [T]).
RequireLongerOrSameLength inp n =>
PeanoNatural n -> Instr inp (Drop n inp)
DROPN PeanoNatural ('S ('S 'Z))
forall (n :: Nat). (n ~ 'S ('S 'Z)) => PeanoNatural n
Two)
Instr inp b
DROP :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (PeanoNatural ('S ('S 'Z)) -> Instr inp (Drop ('S ('S 'Z)) inp)
forall (n :: Nat) (inp :: [T]).
RequireLongerOrSameLength inp n =>
PeanoNatural n -> Instr inp (Drop n inp)
DROPN PeanoNatural ('S ('S 'Z))
forall (n :: Nat). (n ~ 'S ('S 'Z)) => PeanoNatural n
Two Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
specificPush :: Rule
specificPush :: Rule
specificPush = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
push :: Instr inp out
push@PUSH{} -> Instr inp out -> Maybe (Instr inp out)
forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
optimizePush Instr inp out
push
push :: Instr inp b
push@PUSH{} :# Instr b out
c -> (Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c) (Instr inp b -> Instr inp out)
-> Maybe (Instr inp b) -> Maybe (Instr inp out)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Instr inp b -> Maybe (Instr inp b)
forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
optimizePush Instr inp b
push
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
where
optimizePush :: Instr inp out -> Maybe (Instr inp out)
optimizePush :: forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
optimizePush = \case
PUSH Value' Instr t
v | Value' Instr t
_ :: Value v <- Value' Instr t
v -> case Value' Instr t
v of
Value' Instr t
VUnit -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TUnit : s)) =>
Instr inp out
UNIT
VMap Map (Value' Instr k) (Value' Instr v)
m
| Map (Value' Instr k) (Value' Instr v) -> Bool
forall t. Container t => t -> Bool
null Map (Value' Instr k) (Value' Instr v)
m -> case forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @v of STMap{} -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ s, out ~ ('TMap a b : s), SingI a, SingI b, Comparable a) =>
Instr inp out
EMPTY_MAP
VSet Set (Value' Instr t1)
m
| Set (Value' Instr t1) -> Bool
forall t. Container t => t -> Bool
null Set (Value' Instr t1)
m -> case forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @v of STSet{} -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
forall {inp :: [T]} {out :: [T]} (e :: T) (s :: [T]).
(inp ~ s, out ~ ('TSet e : s), SingI e, Comparable e) =>
Instr inp out
EMPTY_SET
Value' Instr t
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
isSomeOnIf :: Rule
isSomeOnIf :: Rule
isSomeOnIf = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
IF (PUSH (VOption Just{})) (PUSH (VOption Maybe (Value' Instr t1)
Nothing)) :# Instr b out
c -> case Instr b out
c of
IF_NONE (PUSH (VBool Bool
False)) (Instr (a : s) b
DROP :# PUSH (VBool Bool
True)) :# Instr b out
s -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
s
IF_NONE (PUSH (VBool Bool
False)) (Instr (a : s) b
DROP :# PUSH (VBool Bool
True)) -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr b out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
pairUnpair :: Rule
pairUnpair :: Rule
pairUnpair = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
Instr inp b
PAIR :# Instr b b
UNPAIR :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
PAIR :# Instr b out
UNPAIR -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp b
UNPAIR :# Instr b b
PAIR :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
Instr inp b
UNPAIR :# Instr b out
PAIR -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
pairMisc :: Rule
pairMisc :: Rule
pairMisc = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
Instr inp b
PAIR :# Instr b b
CDR :# Instr b out
c -> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a. a -> Maybe a
Just (Instr (a : b) out -> Maybe (Instr (a : b) out))
-> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b) b -> Instr b out -> Instr (a : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
PAIR :# Instr b out
CDR -> Instr (a : out) out -> Maybe (Instr (a : out) out)
forall a. a -> Maybe a
Just Instr (a : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
PAIR :# Instr b b
CAR :# Instr b out
c -> Instr (a : b : s) out -> Maybe (Instr (a : b : s) out)
forall a. a -> Maybe a
Just (Instr (a : b : s) out -> Maybe (Instr (a : b : s) out))
-> Instr (a : b : s) out -> Maybe (Instr (a : b : s) out)
forall a b. (a -> b) -> a -> b
$ (Instr (b : s) s -> Instr (a : b : s) (a : s)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr (b : s) s
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP) Instr (a : b : s) (a : s)
-> Instr (a : s) out -> Instr (a : b : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr (a : s) out
c
Instr inp b
PAIR :# Instr b out
CAR -> Instr (a : b : s) (a : s) -> Maybe (Instr (a : b : s) (a : s))
forall a. a -> Maybe a
Just (Instr (a : b : s) (a : s) -> Maybe (Instr (a : b : s) (a : s)))
-> Instr (a : b : s) (a : s) -> Maybe (Instr (a : b : s) (a : s))
forall a b. (a -> b) -> a -> b
$ Instr (b : s) s -> Instr (a : b : s) (a : s)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr (b : s) s
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
unpairMisc :: Rule
unpairMisc :: Rule
unpairMisc = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
Instr inp b
DUP :# Instr b b
CAR :# DIP Instr a c
CDR -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
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 inp b
DUP :# Instr b b
CAR :# DIP Instr a c
CDR :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp b
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 inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
DUP :# Instr b b
CDR :# DIP Instr a c
CAR -> Instr inp (b : a : s) -> Maybe (Instr inp (b : a : s))
forall a. a -> Maybe a
Just (Instr inp (b : a : s) -> Maybe (Instr inp (b : a : s)))
-> Instr inp (b : a : s) -> Maybe (Instr inp (b : a : s))
forall a b. (a -> b) -> a -> b
$ Instr inp (a : b : 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 inp (a : b : s)
-> Instr (a : b : s) (b : a : s) -> Instr inp (b : a : s)
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : b : s) (b : a : s)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP
Instr inp b
DUP :# Instr b b
CDR :# DIP Instr a c
CAR :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp (a : b : 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 inp (a : b : s) -> Instr (a : b : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : b : s) (b : a : s)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP Instr (a : b : s) (b : a : s)
-> Instr (b : a : s) out -> Instr (a : b : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr (b : a : s) out
c
Instr inp b
UNPAIR :# Instr b out
DROP -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (b : s)) =>
Instr inp out
CDR
Instr inp b
UNPAIR :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp b
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (b : s)) =>
Instr inp out
CDR Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
commuteArith ::
forall n m s out. Instr (n ': m ': s) out -> Maybe (Instr (m ': n ': s) out)
commuteArith :: forall (n :: T) (m :: T) (s :: [T]) (out :: [T]).
Instr (n : m : s) out -> Maybe (Instr (m : n : s) out)
commuteArith = \case
Instr (n : m : s) out
ADD -> do Dict (ArithRes Add n m ~ ArithRes Add m n, ArithOp Add m n)
Dict <- forall {k} (aop :: k) (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
forall aop (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
commutativityProof @Add @n @m; Instr (m : n : s) out -> Maybe (Instr (m : n : s) out)
forall a. a -> Maybe a
Just Instr (m : n : s) out
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Add n m : s),
ArithOp Add n m) =>
Instr inp out
ADD
Instr (n : m : s) out
MUL -> do Dict (ArithRes Mul n m ~ ArithRes Mul m n, ArithOp Mul m n)
Dict <- forall {k} (aop :: k) (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
forall aop (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
commutativityProof @Mul @n @m; Instr (m : n : s) out -> Maybe (Instr (m : n : s) out)
forall a. a -> Maybe a
Just Instr (m : n : s) out
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Mul n m : s),
ArithOp Mul n m) =>
Instr inp out
MUL
Instr (n : m : s) out
OR -> do Dict (ArithRes Or n m ~ ArithRes Or m n, ArithOp Or m n)
Dict <- forall {k} (aop :: k) (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
forall aop (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
commutativityProof @Or @n @m; Instr (m : n : s) out -> Maybe (Instr (m : n : s) out)
forall a. a -> Maybe a
Just Instr (m : n : s) out
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Or n m : s), ArithOp Or n m) =>
Instr inp out
OR
Instr (n : m : s) out
AND -> do Dict (ArithRes And n m ~ ArithRes And m n, ArithOp And m n)
Dict <- forall {k} (aop :: k) (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
forall aop (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
commutativityProof @And @n @m; Instr (m : n : s) out -> Maybe (Instr (m : n : s) out)
forall a. a -> Maybe a
Just Instr (m : n : s) out
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes And n m : s),
ArithOp And n m) =>
Instr inp out
AND
Instr (n : m : s) out
XOR -> do Dict (ArithRes Xor n m ~ ArithRes Xor m n, ArithOp Xor m n)
Dict <- forall {k} (aop :: k) (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
forall aop (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
commutativityProof @Xor @n @m; Instr (m : n : s) out -> Maybe (Instr (m : n : s) out)
forall a. a -> Maybe a
Just Instr (m : n : s) out
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Xor n m : s),
ArithOp Xor n m) =>
Instr inp out
XOR
Instr (n : m : s) out
_ -> Maybe (Instr (m : n : s) out)
forall a. Maybe a
Nothing
swapBeforeCommutative :: Rule
swapBeforeCommutative :: Rule
swapBeforeCommutative = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
Instr inp b
SWAP :# Instr b b
i :# Instr b out
c -> (Instr (a : b : s) b -> Instr b out -> Instr (a : b : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c) (Instr (a : b : s) b -> Instr (a : b : s) out)
-> Maybe (Instr (a : b : s) b) -> Maybe (Instr (a : b : s) out)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Instr (b : a : s) b -> Maybe (Instr (a : b : s) b)
forall (n :: T) (m :: T) (s :: [T]) (out :: [T]).
Instr (n : m : s) out -> Maybe (Instr (m : n : s) out)
commuteArith Instr b b
Instr (b : a : s) b
i
Instr inp b
SWAP :# Instr b out
i -> Instr (b : a : s) out -> Maybe (Instr (a : b : s) out)
forall (n :: T) (m :: T) (s :: [T]) (out :: [T]).
Instr (n : m : s) out -> Maybe (Instr (m : n : s) out)
commuteArith Instr b out
Instr (b : a : s) out
i
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
pushPack :: Rule
pushPack :: Rule
pushPack = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
PUSH Value' Instr t
x :# Instr b out
PACK -> Instr inp ('TBytes : inp) -> Maybe (Instr inp ('TBytes : inp))
forall a. a -> Maybe a
Just (Value' Instr t -> Instr inp ('TBytes : inp)
forall (t :: T) (s :: [T]).
PackedValScope t =>
Value t -> Instr s ('TBytes : s)
pushPacked Value' Instr t
x)
PUSH Value' Instr t
x :# Instr b b
PACK :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr t -> Instr inp ('TBytes : inp)
forall (t :: T) (s :: [T]).
PackedValScope t =>
Value t -> Instr s ('TBytes : s)
pushPacked Value' Instr t
x Instr inp ('TBytes : inp)
-> Instr ('TBytes : inp) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr ('TBytes : inp) out
c)
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
where
pushPacked :: PackedValScope t => Value t -> Instr s ('TBytes ': s)
pushPacked :: forall (t :: T) (s :: [T]).
PackedValScope t =>
Value t -> Instr s ('TBytes : s)
pushPacked = Value' Instr 'TBytes -> Instr s ('TBytes : 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 'TBytes -> Instr s ('TBytes : s))
-> (Value t -> Value' Instr 'TBytes)
-> Value t
-> Instr s ('TBytes : s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Value' Instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value' Instr 'TBytes)
-> (Value t -> ByteString) -> Value t -> Value' Instr 'TBytes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value t -> ByteString
forall (t :: T). PackedValScope t => Value t -> ByteString
packValue'
justDrops :: Rule
justDrops :: Rule
justDrops = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
Instr inp b
CAR :# Instr b b
DROP :# Instr b out
c -> Instr ('TPair a b : b) out -> Maybe (Instr ('TPair a b : b) out)
forall a. a -> Maybe a
Just (Instr ('TPair a b : b) out -> Maybe (Instr ('TPair a b : b) out))
-> Instr ('TPair a b : b) out -> Maybe (Instr ('TPair a b : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TPair a b : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TPair a b : b) b
-> Instr b out -> Instr ('TPair a b : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
CDR :# Instr b b
DROP :# Instr b out
c -> Instr ('TPair a b : b) out -> Maybe (Instr ('TPair a b : b) out)
forall a. a -> Maybe a
Just (Instr ('TPair a b : b) out -> Maybe (Instr ('TPair a b : b) out))
-> Instr ('TPair a b : b) out -> Maybe (Instr ('TPair a b : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TPair a b : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TPair a b : b) b
-> Instr b out -> Instr ('TPair a b : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
SOME :# Instr b b
DROP :# Instr b out
c -> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a. a -> Maybe a
Just (Instr (a : b) out -> Maybe (Instr (a : b) out))
-> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b) b -> Instr b out -> Instr (a : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
LEFT :# Instr b b
DROP :# Instr b out
c -> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a. a -> Maybe a
Just (Instr (a : b) out -> Maybe (Instr (a : b) out))
-> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b) b -> Instr b out -> Instr (a : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
RIGHT :# Instr b b
DROP :# Instr b out
c -> Instr (b : b) out -> Maybe (Instr (b : b) out)
forall a. a -> Maybe a
Just (Instr (b : b) out -> Maybe (Instr (b : b) out))
-> Instr (b : b) out -> Maybe (Instr (b : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (b : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (b : b) b -> Instr b out -> Instr (b : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
SIZE :# Instr b b
DROP :# Instr b out
c -> Instr (c : b) out -> Maybe (Instr (c : b) out)
forall a. a -> Maybe a
Just (Instr (c : b) out -> Maybe (Instr (c : b) out))
-> Instr (c : b) out -> Maybe (Instr (c : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (c : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (c : b) b -> Instr b out -> Instr (c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
GETN PeanoNatural ix
_ :# Instr b b
DROP :# Instr b out
c -> Instr (pair : b) out -> Maybe (Instr (pair : b) out)
forall a. a -> Maybe a
Just (Instr (pair : b) out -> Maybe (Instr (pair : b) out))
-> Instr (pair : b) out -> Maybe (Instr (pair : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (pair : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (pair : b) b -> Instr b out -> Instr (pair : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
CAST :# Instr b b
DROP :# Instr b out
c -> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a. a -> Maybe a
Just (Instr (a : b) out -> Maybe (Instr (a : b) out))
-> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b) b -> Instr b out -> Instr (a : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
RENAME :# Instr b b
DROP :# Instr b out
c -> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a. a -> Maybe a
Just (Instr (a : b) out -> Maybe (Instr (a : b) out))
-> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b) b -> Instr b out -> Instr (a : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
PACK :# Instr b b
DROP :# Instr b out
c -> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a. a -> Maybe a
Just (Instr (a : b) out -> Maybe (Instr (a : b) out))
-> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b) b -> Instr b out -> Instr (a : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
UNPACK :# Instr b b
DROP :# Instr b out
c -> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a. a -> Maybe a
Just (Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out))
-> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TBytes : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TBytes : b) b -> Instr b out -> Instr ('TBytes : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
CONCAT' :# Instr b b
DROP :# Instr b out
c -> Instr ('TList c : b) out -> Maybe (Instr ('TList c : b) out)
forall a. a -> Maybe a
Just (Instr ('TList c : b) out -> Maybe (Instr ('TList c : b) out))
-> Instr ('TList c : b) out -> Maybe (Instr ('TList c : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TList c : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TList c : b) b -> Instr b out -> Instr ('TList c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
ISNAT :# Instr b b
DROP :# Instr b out
c -> Instr ('TInt : b) out -> Maybe (Instr ('TInt : b) out)
forall a. a -> Maybe a
Just (Instr ('TInt : b) out -> Maybe (Instr ('TInt : b) out))
-> Instr ('TInt : b) out -> Maybe (Instr ('TInt : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TInt : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TInt : b) b -> Instr b out -> Instr ('TInt : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
ABS :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
NEG :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
NOT :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
EQ :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
NEQ :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
LT :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
GT :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
LE :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
GE :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
INT :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
CONTRACT EpName
_ :# Instr b b
DROP :# Instr b out
c -> Instr ('TAddress : b) out -> Maybe (Instr ('TAddress : b) out)
forall a. a -> Maybe a
Just (Instr ('TAddress : b) out -> Maybe (Instr ('TAddress : b) out))
-> Instr ('TAddress : b) out -> Maybe (Instr ('TAddress : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TAddress : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TAddress : b) b -> Instr b out -> Instr ('TAddress : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
SET_DELEGATE :# Instr b b
DROP :# Instr b out
c -> Instr ('TOption 'TKeyHash : b) out
-> Maybe (Instr ('TOption 'TKeyHash : b) out)
forall a. a -> Maybe a
Just (Instr ('TOption 'TKeyHash : b) out
-> Maybe (Instr ('TOption 'TKeyHash : b) out))
-> Instr ('TOption 'TKeyHash : b) out
-> Maybe (Instr ('TOption 'TKeyHash : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TOption 'TKeyHash : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TOption 'TKeyHash : b) b
-> Instr b out -> Instr ('TOption 'TKeyHash : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
IMPLICIT_ACCOUNT :# Instr b b
DROP :# Instr b out
c -> Instr ('TKeyHash : b) out -> Maybe (Instr ('TKeyHash : b) out)
forall a. a -> Maybe a
Just (Instr ('TKeyHash : b) out -> Maybe (Instr ('TKeyHash : b) out))
-> Instr ('TKeyHash : b) out -> Maybe (Instr ('TKeyHash : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TKeyHash : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TKeyHash : b) b -> Instr b out -> Instr ('TKeyHash : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
VOTING_POWER :# Instr b b
DROP :# Instr b out
c -> Instr ('TKeyHash : b) out -> Maybe (Instr ('TKeyHash : b) out)
forall a. a -> Maybe a
Just (Instr ('TKeyHash : b) out -> Maybe (Instr ('TKeyHash : b) out))
-> Instr ('TKeyHash : b) out -> Maybe (Instr ('TKeyHash : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TKeyHash : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TKeyHash : b) b -> Instr b out -> Instr ('TKeyHash : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
SHA256 :# Instr b b
DROP :# Instr b out
c -> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a. a -> Maybe a
Just (Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out))
-> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TBytes : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TBytes : b) b -> Instr b out -> Instr ('TBytes : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
SHA512 :# Instr b b
DROP :# Instr b out
c -> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a. a -> Maybe a
Just (Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out))
-> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TBytes : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TBytes : b) b -> Instr b out -> Instr ('TBytes : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
BLAKE2B :# Instr b b
DROP :# Instr b out
c -> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a. a -> Maybe a
Just (Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out))
-> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TBytes : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TBytes : b) b -> Instr b out -> Instr ('TBytes : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
SHA3 :# Instr b b
DROP :# Instr b out
c -> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a. a -> Maybe a
Just (Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out))
-> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TBytes : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TBytes : b) b -> Instr b out -> Instr ('TBytes : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
KECCAK :# Instr b b
DROP :# Instr b out
c -> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a. a -> Maybe a
Just (Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out))
-> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TBytes : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TBytes : b) b -> Instr b out -> Instr ('TBytes : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
HASH_KEY :# Instr b b
DROP :# Instr b out
c -> Instr ('TKey : b) out -> Maybe (Instr ('TKey : b) out)
forall a. a -> Maybe a
Just (Instr ('TKey : b) out -> Maybe (Instr ('TKey : b) out))
-> Instr ('TKey : b) out -> Maybe (Instr ('TKey : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TKey : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TKey : b) b -> Instr b out -> Instr ('TKey : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
PAIRING_CHECK :# Instr b b
DROP :# Instr b out
c -> Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) out
-> Maybe
(Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) out)
forall a. a -> Maybe a
Just (Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) out
-> Maybe
(Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) out))
-> Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) out
-> Maybe
(Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) b
-> Instr b out
-> Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
ADDRESS :# Instr b b
DROP :# Instr b out
c -> Instr ('TContract a : b) out
-> Maybe (Instr ('TContract a : b) out)
forall a. a -> Maybe a
Just (Instr ('TContract a : b) out
-> Maybe (Instr ('TContract a : b) out))
-> Instr ('TContract a : b) out
-> Maybe (Instr ('TContract a : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TContract a : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TContract a : b) b
-> Instr b out -> Instr ('TContract a : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
JOIN_TICKETS :# Instr b b
DROP :# Instr b out
c -> Instr ('TPair ('TTicket a) ('TTicket a) : b) out
-> Maybe (Instr ('TPair ('TTicket a) ('TTicket a) : b) out)
forall a. a -> Maybe a
Just (Instr ('TPair ('TTicket a) ('TTicket a) : b) out
-> Maybe (Instr ('TPair ('TTicket a) ('TTicket a) : b) out))
-> Instr ('TPair ('TTicket a) ('TTicket a) : b) out
-> Maybe (Instr ('TPair ('TTicket a) ('TTicket a) : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TPair ('TTicket a) ('TTicket a) : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TPair ('TTicket a) ('TTicket a) : b) b
-> Instr b out -> Instr ('TPair ('TTicket a) ('TTicket a) : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
CAR :# Instr b out
DROP -> Instr ('TPair a b : out) out
-> Maybe (Instr ('TPair a b : out) out)
forall a. a -> Maybe a
Just Instr ('TPair a b : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
CDR :# Instr b out
DROP -> Instr ('TPair a b : out) out
-> Maybe (Instr ('TPair a b : out) out)
forall a. a -> Maybe a
Just Instr ('TPair a b : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
SOME :# Instr b out
DROP -> Instr (a : out) out -> Maybe (Instr (a : out) out)
forall a. a -> Maybe a
Just Instr (a : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
LEFT :# Instr b out
DROP -> Instr (a : out) out -> Maybe (Instr (a : out) out)
forall a. a -> Maybe a
Just Instr (a : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
RIGHT :# Instr b out
DROP -> Instr (b : out) out -> Maybe (Instr (b : out) out)
forall a. a -> Maybe a
Just Instr (b : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
SIZE :# Instr b out
DROP -> Instr (c : out) out -> Maybe (Instr (c : out) out)
forall a. a -> Maybe a
Just Instr (c : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
GETN PeanoNatural ix
_ :# Instr b out
DROP -> Instr (pair : out) out -> Maybe (Instr (pair : out) out)
forall a. a -> Maybe a
Just Instr (pair : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
CAST :# Instr b out
DROP -> Instr (a : out) out -> Maybe (Instr (a : out) out)
forall a. a -> Maybe a
Just Instr (a : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
RENAME :# Instr b out
DROP -> Instr (a : out) out -> Maybe (Instr (a : out) out)
forall a. a -> Maybe a
Just Instr (a : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
PACK :# Instr b out
DROP -> Instr (a : out) out -> Maybe (Instr (a : out) out)
forall a. a -> Maybe a
Just Instr (a : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
UNPACK :# Instr b out
DROP -> Instr ('TBytes : out) out -> Maybe (Instr ('TBytes : out) out)
forall a. a -> Maybe a
Just Instr ('TBytes : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
CONCAT' :# Instr b out
DROP -> Instr ('TList c : out) out -> Maybe (Instr ('TList c : out) out)
forall a. a -> Maybe a
Just Instr ('TList c : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
ISNAT :# Instr b out
DROP -> Instr ('TInt : out) out -> Maybe (Instr ('TInt : out) out)
forall a. a -> Maybe a
Just Instr ('TInt : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
ABS :# Instr b out
DROP -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
NEG :# Instr b out
DROP -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
NOT :# Instr b out
DROP -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
EQ :# Instr b out
DROP -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
NEQ :# Instr b out
DROP -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
LT :# Instr b out
DROP -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
GT :# Instr b out
DROP -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
LE :# Instr b out
DROP -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
GE :# Instr b out
DROP -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
INT :# Instr b out
DROP -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
CONTRACT EpName
_ :# Instr b out
DROP -> Instr ('TAddress : out) out -> Maybe (Instr ('TAddress : out) out)
forall a. a -> Maybe a
Just Instr ('TAddress : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
SET_DELEGATE :# Instr b out
DROP -> Instr ('TOption 'TKeyHash : out) out
-> Maybe (Instr ('TOption 'TKeyHash : out) out)
forall a. a -> Maybe a
Just Instr ('TOption 'TKeyHash : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
IMPLICIT_ACCOUNT :# Instr b out
DROP -> Instr ('TKeyHash : out) out -> Maybe (Instr ('TKeyHash : out) out)
forall a. a -> Maybe a
Just Instr ('TKeyHash : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
VOTING_POWER :# Instr b out
DROP -> Instr ('TKeyHash : out) out -> Maybe (Instr ('TKeyHash : out) out)
forall a. a -> Maybe a
Just Instr ('TKeyHash : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
SHA256 :# Instr b out
DROP -> Instr ('TBytes : out) out -> Maybe (Instr ('TBytes : out) out)
forall a. a -> Maybe a
Just Instr ('TBytes : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
SHA512 :# Instr b out
DROP -> Instr ('TBytes : out) out -> Maybe (Instr ('TBytes : out) out)
forall a. a -> Maybe a
Just Instr ('TBytes : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
BLAKE2B :# Instr b out
DROP -> Instr ('TBytes : out) out -> Maybe (Instr ('TBytes : out) out)
forall a. a -> Maybe a
Just Instr ('TBytes : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
SHA3 :# Instr b out
DROP -> Instr ('TBytes : out) out -> Maybe (Instr ('TBytes : out) out)
forall a. a -> Maybe a
Just Instr ('TBytes : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
KECCAK :# Instr b out
DROP -> Instr ('TBytes : out) out -> Maybe (Instr ('TBytes : out) out)
forall a. a -> Maybe a
Just Instr ('TBytes : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
HASH_KEY :# Instr b out
DROP -> Instr ('TKey : out) out -> Maybe (Instr ('TKey : out) out)
forall a. a -> Maybe a
Just Instr ('TKey : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
PAIRING_CHECK :# Instr b out
DROP -> Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : out) out
-> Maybe
(Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : out) out)
forall a. a -> Maybe a
Just Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
ADDRESS :# Instr b out
DROP -> Instr ('TContract a : out) out
-> Maybe (Instr ('TContract a : out) out)
forall a. a -> Maybe a
Just Instr ('TContract a : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
JOIN_TICKETS :# Instr b out
DROP -> Instr ('TPair ('TTicket a) ('TTicket a) : out) out
-> Maybe (Instr ('TPair ('TTicket a) ('TTicket a) : out) out)
forall a. a -> Maybe a
Just Instr ('TPair ('TTicket a) ('TTicket a) : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
justDoubleDrops :: Rule
justDoubleDrops :: Rule
justDoubleDrops = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
Instr inp b
PAIR :# Instr b b
DROP :# Instr b out
c -> Instr (a : b : b) out -> Maybe (Instr (a : b : b) out)
forall a. a -> Maybe a
Just (Instr (a : b : b) out -> Maybe (Instr (a : b : b) out))
-> Instr (a : b : b) out -> Maybe (Instr (a : b : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b : b) (b : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b : b) (b : b)
-> Instr (b : b) out -> Instr (a : b : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (b : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (b : b) b -> Instr b out -> Instr (b : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
MEM :# Instr b b
DROP :# Instr b out
c -> Instr (MemOpKey c : c : b) out
-> Maybe (Instr (MemOpKey c : c : b) out)
forall a. a -> Maybe a
Just (Instr (MemOpKey c : c : b) out
-> Maybe (Instr (MemOpKey c : c : b) out))
-> Instr (MemOpKey c : c : b) out
-> Maybe (Instr (MemOpKey c : c : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (MemOpKey c : c : b) (c : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (MemOpKey c : c : b) (c : b)
-> Instr (c : b) out -> Instr (MemOpKey c : c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (c : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (c : b) b -> Instr b out -> Instr (c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
GET :# Instr b b
DROP :# Instr b out
c -> Instr (GetOpKey c : c : b) out
-> Maybe (Instr (GetOpKey c : c : b) out)
forall a. a -> Maybe a
Just (Instr (GetOpKey c : c : b) out
-> Maybe (Instr (GetOpKey c : c : b) out))
-> Instr (GetOpKey c : c : b) out
-> Maybe (Instr (GetOpKey c : c : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (GetOpKey c : c : b) (c : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (GetOpKey c : c : b) (c : b)
-> Instr (c : b) out -> Instr (GetOpKey c : c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (c : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (c : b) b -> Instr b out -> Instr (c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
APPLY :# Instr b b
DROP :# Instr b out
c -> Instr (a : 'TLambda ('TPair a b) c : b) out
-> Maybe (Instr (a : 'TLambda ('TPair a b) c : b) out)
forall a. a -> Maybe a
Just (Instr (a : 'TLambda ('TPair a b) c : b) out
-> Maybe (Instr (a : 'TLambda ('TPair a b) c : b) out))
-> Instr (a : 'TLambda ('TPair a b) c : b) out
-> Maybe (Instr (a : 'TLambda ('TPair a b) c : b) out)
forall a b. (a -> b) -> a -> b
$ Instr
(a : 'TLambda ('TPair a b) c : b) ('TLambda ('TPair a b) c : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr
(a : 'TLambda ('TPair a b) c : b) ('TLambda ('TPair a b) c : b)
-> Instr ('TLambda ('TPair a b) c : b) out
-> Instr (a : 'TLambda ('TPair a b) c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TLambda ('TPair a b) c : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TLambda ('TPair a b) c : b) b
-> Instr b out -> Instr ('TLambda ('TPair a b) c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
CONCAT :# Instr b b
DROP :# Instr b out
c -> Instr (c : c : b) out -> Maybe (Instr (c : c : b) out)
forall a. a -> Maybe a
Just (Instr (c : c : b) out -> Maybe (Instr (c : c : b) out))
-> Instr (c : c : b) out -> Maybe (Instr (c : c : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (c : c : b) (c : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (c : c : b) (c : b)
-> Instr (c : b) out -> Instr (c : c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (c : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (c : b) b -> Instr b out -> Instr (c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
ADD :# Instr b b
DROP :# Instr b out
c -> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a. a -> Maybe a
Just (Instr (n : m : b) out -> Maybe (Instr (n : m : b) out))
-> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : b) (m : b)
-> Instr (m : b) out -> Instr (n : m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (m : b) b -> Instr b out -> Instr (m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
SUB :# Instr b b
DROP :# Instr b out
c -> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a. a -> Maybe a
Just (Instr (n : m : b) out -> Maybe (Instr (n : m : b) out))
-> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : b) (m : b)
-> Instr (m : b) out -> Instr (n : m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (m : b) b -> Instr b out -> Instr (m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
SUB_MUTEZ :# Instr b b
DROP :# Instr b out
c -> Instr ('TMutez : 'TMutez : b) out
-> Maybe (Instr ('TMutez : 'TMutez : b) out)
forall a. a -> Maybe a
Just (Instr ('TMutez : 'TMutez : b) out
-> Maybe (Instr ('TMutez : 'TMutez : b) out))
-> Instr ('TMutez : 'TMutez : b) out
-> Maybe (Instr ('TMutez : 'TMutez : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TMutez : 'TMutez : b) ('TMutez : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TMutez : 'TMutez : b) ('TMutez : b)
-> Instr ('TMutez : b) out -> Instr ('TMutez : 'TMutez : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TMutez : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TMutez : b) b -> Instr b out -> Instr ('TMutez : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
MUL :# Instr b b
DROP :# Instr b out
c -> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a. a -> Maybe a
Just (Instr (n : m : b) out -> Maybe (Instr (n : m : b) out))
-> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : b) (m : b)
-> Instr (m : b) out -> Instr (n : m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (m : b) b -> Instr b out -> Instr (m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
EDIV :# Instr b b
DROP :# Instr b out
c -> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a. a -> Maybe a
Just (Instr (n : m : b) out -> Maybe (Instr (n : m : b) out))
-> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : b) (m : b)
-> Instr (m : b) out -> Instr (n : m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (m : b) b -> Instr b out -> Instr (m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
OR :# Instr b b
DROP :# Instr b out
c -> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a. a -> Maybe a
Just (Instr (n : m : b) out -> Maybe (Instr (n : m : b) out))
-> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : b) (m : b)
-> Instr (m : b) out -> Instr (n : m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (m : b) b -> Instr b out -> Instr (m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
AND :# Instr b b
DROP :# Instr b out
c -> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a. a -> Maybe a
Just (Instr (n : m : b) out -> Maybe (Instr (n : m : b) out))
-> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : b) (m : b)
-> Instr (m : b) out -> Instr (n : m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (m : b) b -> Instr b out -> Instr (m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
XOR :# Instr b b
DROP :# Instr b out
c -> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a. a -> Maybe a
Just (Instr (n : m : b) out -> Maybe (Instr (n : m : b) out))
-> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : b) (m : b)
-> Instr (m : b) out -> Instr (n : m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (m : b) b -> Instr b out -> Instr (m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
COMPARE :# Instr b b
DROP :# Instr b out
c -> Instr (n : n : b) out -> Maybe (Instr (n : n : b) out)
forall a. a -> Maybe a
Just (Instr (n : n : b) out -> Maybe (Instr (n : n : b) out))
-> Instr (n : n : b) out -> Maybe (Instr (n : n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : n : b) (n : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : n : b) (n : b)
-> Instr (n : b) out -> Instr (n : n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
TICKET :# Instr b b
DROP :# Instr b out
c -> Instr (a : 'TNat : b) out -> Maybe (Instr (a : 'TNat : b) out)
forall a. a -> Maybe a
Just (Instr (a : 'TNat : b) out -> Maybe (Instr (a : 'TNat : b) out))
-> Instr (a : 'TNat : b) out -> Maybe (Instr (a : 'TNat : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : 'TNat : b) ('TNat : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : 'TNat : b) ('TNat : b)
-> Instr ('TNat : b) out -> Instr (a : 'TNat : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TNat : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TNat : b) b -> Instr b out -> Instr ('TNat : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
SPLIT_TICKET :# Instr b b
DROP :# Instr b out
c -> Instr ('TTicket a : 'TPair 'TNat 'TNat : b) out
-> Maybe (Instr ('TTicket a : 'TPair 'TNat 'TNat : b) out)
forall a. a -> Maybe a
Just (Instr ('TTicket a : 'TPair 'TNat 'TNat : b) out
-> Maybe (Instr ('TTicket a : 'TPair 'TNat 'TNat : b) out))
-> Instr ('TTicket a : 'TPair 'TNat 'TNat : b) out
-> Maybe (Instr ('TTicket a : 'TPair 'TNat 'TNat : b) out)
forall a b. (a -> b) -> a -> b
$ Instr
('TTicket a : 'TPair 'TNat 'TNat : b) ('TPair 'TNat 'TNat : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr
('TTicket a : 'TPair 'TNat 'TNat : b) ('TPair 'TNat 'TNat : b)
-> Instr ('TPair 'TNat 'TNat : b) out
-> Instr ('TTicket a : 'TPair 'TNat 'TNat : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TPair 'TNat 'TNat : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TPair 'TNat 'TNat : b) b
-> Instr b out -> Instr ('TPair 'TNat 'TNat : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
SWAP :# Instr b b
DROP :# Instr b b
DROP :# Instr b out
c -> Instr (a : b : b) out -> Maybe (Instr (a : b : b) out)
forall a. a -> Maybe a
Just (Instr (a : b : b) out -> Maybe (Instr (a : b : b) out))
-> Instr (a : b : b) out -> Maybe (Instr (a : b : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b : b) (b : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b : b) (b : b)
-> Instr (b : b) out -> Instr (a : b : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (b : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (b : b) b -> Instr b out -> Instr (b : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
Instr inp b
PAIR :# Instr b out
DROP -> Instr (a : b : out) out -> Maybe (Instr (a : b : out) out)
forall a. a -> Maybe a
Just (Instr (a : b : out) out -> Maybe (Instr (a : b : out) out))
-> Instr (a : b : out) out -> Maybe (Instr (a : b : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b : out) (b : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b : out) (b : out)
-> Instr (b : out) out -> Instr (a : b : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (b : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
MEM :# Instr b out
DROP -> Instr (MemOpKey c : c : out) out
-> Maybe (Instr (MemOpKey c : c : out) out)
forall a. a -> Maybe a
Just (Instr (MemOpKey c : c : out) out
-> Maybe (Instr (MemOpKey c : c : out) out))
-> Instr (MemOpKey c : c : out) out
-> Maybe (Instr (MemOpKey c : c : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (MemOpKey c : c : out) (c : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (MemOpKey c : c : out) (c : out)
-> Instr (c : out) out -> Instr (MemOpKey c : c : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (c : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
GET :# Instr b out
DROP -> Instr (GetOpKey c : c : out) out
-> Maybe (Instr (GetOpKey c : c : out) out)
forall a. a -> Maybe a
Just (Instr (GetOpKey c : c : out) out
-> Maybe (Instr (GetOpKey c : c : out) out))
-> Instr (GetOpKey c : c : out) out
-> Maybe (Instr (GetOpKey c : c : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (GetOpKey c : c : out) (c : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (GetOpKey c : c : out) (c : out)
-> Instr (c : out) out -> Instr (GetOpKey c : c : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (c : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
APPLY :# Instr b out
DROP -> Instr (a : 'TLambda ('TPair a b) c : out) out
-> Maybe (Instr (a : 'TLambda ('TPair a b) c : out) out)
forall a. a -> Maybe a
Just (Instr (a : 'TLambda ('TPair a b) c : out) out
-> Maybe (Instr (a : 'TLambda ('TPair a b) c : out) out))
-> Instr (a : 'TLambda ('TPair a b) c : out) out
-> Maybe (Instr (a : 'TLambda ('TPair a b) c : out) out)
forall a b. (a -> b) -> a -> b
$ Instr
(a : 'TLambda ('TPair a b) c : out) ('TLambda ('TPair a b) c : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr
(a : 'TLambda ('TPair a b) c : out) ('TLambda ('TPair a b) c : out)
-> Instr ('TLambda ('TPair a b) c : out) out
-> Instr (a : 'TLambda ('TPair a b) c : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TLambda ('TPair a b) c : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
CONCAT :# Instr b out
DROP -> Instr (c : c : out) out -> Maybe (Instr (c : c : out) out)
forall a. a -> Maybe a
Just (Instr (c : c : out) out -> Maybe (Instr (c : c : out) out))
-> Instr (c : c : out) out -> Maybe (Instr (c : c : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (c : c : out) (c : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (c : c : out) (c : out)
-> Instr (c : out) out -> Instr (c : c : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (c : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
ADD :# Instr b out
DROP -> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a. a -> Maybe a
Just (Instr (n : m : out) out -> Maybe (Instr (n : m : out) out))
-> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : out) (m : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : out) (m : out)
-> Instr (m : out) out -> Instr (n : m : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
SUB :# Instr b out
DROP -> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a. a -> Maybe a
Just (Instr (n : m : out) out -> Maybe (Instr (n : m : out) out))
-> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : out) (m : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : out) (m : out)
-> Instr (m : out) out -> Instr (n : m : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
SUB_MUTEZ :# Instr b out
DROP -> Instr ('TMutez : 'TMutez : out) out
-> Maybe (Instr ('TMutez : 'TMutez : out) out)
forall a. a -> Maybe a
Just (Instr ('TMutez : 'TMutez : out) out
-> Maybe (Instr ('TMutez : 'TMutez : out) out))
-> Instr ('TMutez : 'TMutez : out) out
-> Maybe (Instr ('TMutez : 'TMutez : out) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TMutez : 'TMutez : out) ('TMutez : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TMutez : 'TMutez : out) ('TMutez : out)
-> Instr ('TMutez : out) out -> Instr ('TMutez : 'TMutez : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TMutez : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
MUL :# Instr b out
DROP -> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a. a -> Maybe a
Just (Instr (n : m : out) out -> Maybe (Instr (n : m : out) out))
-> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : out) (m : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : out) (m : out)
-> Instr (m : out) out -> Instr (n : m : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
EDIV :# Instr b out
DROP -> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a. a -> Maybe a
Just (Instr (n : m : out) out -> Maybe (Instr (n : m : out) out))
-> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : out) (m : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : out) (m : out)
-> Instr (m : out) out -> Instr (n : m : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
OR :# Instr b out
DROP -> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a. a -> Maybe a
Just (Instr (n : m : out) out -> Maybe (Instr (n : m : out) out))
-> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : out) (m : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : out) (m : out)
-> Instr (m : out) out -> Instr (n : m : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
AND :# Instr b out
DROP -> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a. a -> Maybe a
Just (Instr (n : m : out) out -> Maybe (Instr (n : m : out) out))
-> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : out) (m : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : out) (m : out)
-> Instr (m : out) out -> Instr (n : m : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
XOR :# Instr b out
DROP -> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a. a -> Maybe a
Just (Instr (n : m : out) out -> Maybe (Instr (n : m : out) out))
-> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : out) (m : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : out) (m : out)
-> Instr (m : out) out -> Instr (n : m : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
COMPARE :# Instr b out
DROP -> Instr (n : n : out) out -> Maybe (Instr (n : n : out) out)
forall a. a -> Maybe a
Just (Instr (n : n : out) out -> Maybe (Instr (n : n : out) out))
-> Instr (n : n : out) out -> Maybe (Instr (n : n : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : n : out) (n : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : n : out) (n : out)
-> Instr (n : out) out -> Instr (n : n : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
TICKET :# Instr b out
DROP -> Instr (a : 'TNat : out) out -> Maybe (Instr (a : 'TNat : out) out)
forall a. a -> Maybe a
Just (Instr (a : 'TNat : out) out
-> Maybe (Instr (a : 'TNat : out) out))
-> Instr (a : 'TNat : out) out
-> Maybe (Instr (a : 'TNat : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : 'TNat : out) ('TNat : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : 'TNat : out) ('TNat : out)
-> Instr ('TNat : out) out -> Instr (a : 'TNat : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TNat : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
SPLIT_TICKET :# Instr b out
DROP -> Instr ('TTicket a : 'TPair 'TNat 'TNat : out) out
-> Maybe (Instr ('TTicket a : 'TPair 'TNat 'TNat : out) out)
forall a. a -> Maybe a
Just (Instr ('TTicket a : 'TPair 'TNat 'TNat : out) out
-> Maybe (Instr ('TTicket a : 'TPair 'TNat 'TNat : out) out))
-> Instr ('TTicket a : 'TPair 'TNat 'TNat : out) out
-> Maybe (Instr ('TTicket a : 'TPair 'TNat 'TNat : out) out)
forall a b. (a -> b) -> a -> b
$ Instr
('TTicket a : 'TPair 'TNat 'TNat : out) ('TPair 'TNat 'TNat : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr
('TTicket a : 'TPair 'TNat 'TNat : out) ('TPair 'TNat 'TNat : out)
-> Instr ('TPair 'TNat 'TNat : out) out
-> Instr ('TTicket a : 'TPair 'TNat 'TNat : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TPair 'TNat 'TNat : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp b
SWAP :# Instr b b
DROP :# Instr b out
DROP -> Instr (a : b : out) out -> Maybe (Instr (a : b : out) out)
forall a. a -> Maybe a
Just (Instr (a : b : out) out -> Maybe (Instr (a : b : out) out))
-> Instr (a : b : out) out -> Maybe (Instr (a : b : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b : out) (b : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b : out) (b : out)
-> Instr (b : out) out -> Instr (a : b : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (b : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
linearizeAndReapply :: Rule -> Instr inp out -> Instr inp out
linearizeAndReapply :: forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
linearizeAndReapply Rule
restart = \case
Seq (Seq Instr inp b
a Instr b b
b) Instr b out
c ->
Rule -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
applyOnce Rule
restart (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 Instr inp b
a (Rule -> Instr b out -> Instr b out
forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
linearizeAndReapply Rule
restart (Instr b b -> Instr b out -> Instr b out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr b b
b Instr b out
c))
Instr inp out
other -> Rule -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
applyOnce Rule
restart Instr inp out
other
orRule :: (Rule -> Rule) -> (Rule -> Rule) -> (Rule -> Rule)
orRule :: (Rule -> Rule) -> (Rule -> Rule) -> Rule -> Rule
orRule Rule -> Rule
l Rule -> Rule
r Rule
topl = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \Instr inp out
instr ->
(Rule
-> forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
unRule (Rule -> Rule
l Rule
topl) (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
instr) Maybe (Instr inp out)
-> Maybe (Instr inp out) -> Maybe (Instr inp out)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Rule
-> forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
unRule (Rule -> Rule
r Rule
topl) (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
instr)
orSimpleRule :: (Rule -> Rule) -> Rule -> (Rule -> Rule)
orSimpleRule :: (Rule -> Rule) -> Rule -> Rule -> Rule
orSimpleRule Rule -> Rule
l Rule
r Rule
topl = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule)
-> (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \Instr inp out
instr ->
(Rule
-> forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
unRule (Rule -> Rule
l Rule
topl) (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
instr) Maybe (Instr inp out)
-> Maybe (Instr inp out) -> Maybe (Instr inp out)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Rule
-> forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
unRule Rule
r (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
instr)
fixpoint :: (Rule -> Rule) -> Rule
fixpoint :: (Rule -> Rule) -> Rule
fixpoint Rule -> Rule
r = Rule
go
where
go :: Rule
go :: Rule
go = Rule -> Rule
whileApplies (Rule -> Rule
r Rule
go)
applyOnce :: Rule -> Instr inp out -> Instr inp out
applyOnce :: forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
applyOnce Rule
r Instr inp out
i = Instr inp out
-> (Instr inp out -> Instr inp out)
-> Maybe (Instr inp out)
-> Instr inp out
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Instr inp out
i Instr inp out -> Instr inp out
forall a. a -> a
id (Rule
-> forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
unRule Rule
r (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
i)
whileApplies :: Rule -> Rule
whileApplies :: Rule -> Rule
whileApplies Rule
r = (forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
go
where
go :: Instr inp out -> Maybe (Instr inp out)
go :: forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
go Instr inp out
i = Maybe (Instr inp out)
-> (Instr inp out -> Maybe (Instr inp out))
-> Maybe (Instr inp out)
-> Maybe (Instr inp out)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
i) Instr inp out -> Maybe (Instr inp out)
forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
go (Rule
-> forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
unRule Rule
r (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
i)
makeLensesFor [("ocGotoValues", "ocGotoValuesL")] ''OptimizerConf