{-# 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 Unsafe.Coerce (unsafeCoerce)
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.Peano
import Morley.Util.PeanoNatural
import Morley.Util.Type
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 Value' Instr ('TLambda 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 Value' Instr ('TLambda 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 ((inp ~ b) => Maybe (Instr inp out))
-> (inp :~: b) -> Maybe (Instr inp out)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [T]) (out :: [T]) (t :: [T]) (n :: Nat) (a :: T).
(KnownList inp, inp ~ (Take n inp ++ (a : Drop ('S n) inp)),
t ~ (a : (Take n inp ++ Drop ('S n) inp)),
out ~ (Take n (Drop ('S 'Z) t) ++ (a : Drop ('S n) t))) =>
SingNat n -> inp :~: out
forall {k} (inp :: [k]) (out :: [k]) (t :: [k]) (n :: Nat)
(a :: k).
(KnownList inp, inp ~ (Take n inp ++ (a : Drop ('S n) inp)),
t ~ (a : (Take n inp ++ Drop ('S n) inp)),
out ~ (Take n (Drop ('S 'Z) t) ++ (a : Drop ('S n) t))) =>
SingNat n -> inp :~: out
digDugProof @inp @out @t @n (PeanoNatural n -> SingNat n
forall (a :: Nat). PeanoNatural a -> SingNat a
singPeanoNat PeanoNatural n
x)
(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 out out -> Maybe (Instr out out)
forall a. a -> Maybe a
Just Instr out out
forall (inp :: [T]). Instr inp inp
Nop ((inp ~ out) => Maybe (Instr inp out))
-> (inp :~: out) -> Maybe (Instr inp out)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [T]) (out :: [T]) (t :: [T]) (n :: Nat) (a :: T).
(KnownList inp, inp ~ (Take n inp ++ (a : Drop ('S n) inp)),
t ~ (a : (Take n inp ++ Drop ('S n) inp)),
out ~ (Take n (Drop ('S 'Z) t) ++ (a : Drop ('S n) t))) =>
SingNat n -> inp :~: out
forall {k} (inp :: [k]) (out :: [k]) (t :: [k]) (n :: Nat)
(a :: k).
(KnownList inp, inp ~ (Take n inp ++ (a : Drop ('S n) inp)),
t ~ (a : (Take n inp ++ Drop ('S n) inp)),
out ~ (Take n (Drop ('S 'Z) t) ++ (a : Drop ('S n) t))) =>
SingNat n -> inp :~: out
digDugProof @inp @out @t @n (PeanoNatural n -> SingNat n
forall (a :: Nat). PeanoNatural a -> SingNat a
singPeanoNat PeanoNatural n
x)
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
digDugProof
:: forall inp out t n a.
( KnownList inp
, inp ~ (Take n inp ++ (a ': Drop ('S n) inp))
, t ~ (a ': Take n inp ++ Drop ('S n) inp)
, out ~ (Take n (Drop ('S 'Z) t) ++ (a ': Drop ('S n) t))
)
=> SingNat n -> inp :~: out
{-# RULES "digDugProof" forall n. digDugProof n = unsafeCoerce Refl #-}
{-# INLINE[1] digDugProof #-}
digDugProof :: forall {k} (inp :: [k]) (out :: [k]) (t :: [k]) (n :: Nat)
(a :: k).
(KnownList inp, inp ~ (Take n inp ++ (a : Drop ('S n) inp)),
t ~ (a : (Take n inp ++ Drop ('S n) inp)),
out ~ (Take n (Drop ('S 'Z) t) ++ (a : Drop ('S n) t))) =>
SingNat n -> inp :~: out
digDugProof SingNat n
n = (Take n inp ~ Take n (Take n inp ++ Drop ('S n) inp)) =>
inp :~: out
forall {k} (a :: k). a :~: a
Refl
((Take n inp ~ Take n (Take n inp ++ Drop ('S n) inp)) =>
inp :~: out)
-> (Take n inp :~: Take n (Take n inp ++ Drop ('S n) inp))
-> inp :~: out
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingNat n
-> KList inp
-> Take n inp :~: Take n (Take n inp ++ Drop ('S n) inp)
forall {k} (xs :: [k]) (m :: Nat).
SingNat m
-> KList xs -> Take m xs :~: Take m (Take m xs ++ Drop ('S m) xs)
lemma1 SingNat n
n KList inp
inpS
((Drop ('S n) inp ~ Drop n (Take n inp ++ Drop ('S n) inp)) =>
inp :~: out)
-> (Drop ('S n) inp :~: Drop n (Take n inp ++ Drop ('S n) inp))
-> inp :~: out
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingNat n
-> KList inp
-> Drop ('S n) inp :~: Drop n (Take n inp ++ Drop ('S n) inp)
forall {k} (xs :: [k]) (m :: Nat).
SingNat m
-> KList xs
-> Drop ('S m) xs :~: Drop m (Take m xs ++ Drop ('S m) xs)
lemma2 SingNat n
n KList inp
inpS
where
inpS :: KList inp
inpS = forall (l :: [k]). KnownList l => KList l
forall {k} (l :: [k]). KnownList l => KList l
klist @inp
lemma1 :: forall xs m. SingNat m -> KList xs -> Take m xs :~: Take m (Take m xs ++ Drop ('S m) xs)
lemma1 :: forall {k} (xs :: [k]) (m :: Nat).
SingNat m
-> KList xs -> Take m xs :~: Take m (Take m xs ++ Drop ('S m) xs)
lemma1 = \case
SingNat m
SZ -> ('[] :~: '[]) -> KList xs -> '[] :~: '[]
forall a b. a -> b -> a
const '[] :~: '[]
forall {k} (a :: k). a :~: a
Refl
SS Sing n
m -> \case
KList xs
KNil -> Take m xs :~: Take m (Take m xs ++ Drop ('S m) xs)
forall {k} (a :: k). a :~: a
Refl
KCons Proxy x
_ (Proxy xs
Proxy :: Proxy ys) -> (Take n xs ~ Take n (Take n xs ++ Drop ('S n) xs)) =>
(x : Take n xs) :~: (x : Take n (Take n xs ++ Drop ('S n) xs))
forall {k} (a :: k). a :~: a
Refl ((Take n xs ~ Take n (Take n xs ++ Drop ('S n) xs)) =>
(x : Take n xs) :~: (x : Take n (Take n xs ++ Drop ('S n) xs)))
-> (Take n xs :~: Take n (Take n xs ++ Drop ('S n) xs))
-> (x : Take n xs) :~: (x : Take n (Take n xs ++ Drop ('S n) xs))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingNat n
-> KList xs -> Take n xs :~: Take n (Take n xs ++ Drop ('S n) xs)
forall {k} (xs :: [k]) (m :: Nat).
SingNat m
-> KList xs -> Take m xs :~: Take m (Take m xs ++ Drop ('S m) xs)
lemma1 Sing n
SingNat n
m (forall (l :: [k]). KnownList l => KList l
forall {k} (l :: [k]). KnownList l => KList l
klist @ys)
lemma2 :: forall xs m. SingNat m -> KList xs -> Drop ('S m) xs :~: Drop m (Take m xs ++ Drop ('S m) xs)
lemma2 :: forall {k} (xs :: [k]) (m :: Nat).
SingNat m
-> KList xs
-> Drop ('S m) xs :~: Drop m (Take m xs ++ Drop ('S m) xs)
lemma2 = \case
SingNat m
SZ -> (Drop ('S 'Z) xs :~: Drop ('S 'Z) xs)
-> KList xs -> Drop ('S 'Z) xs :~: Drop ('S 'Z) xs
forall a b. a -> b -> a
const Drop ('S 'Z) xs :~: Drop ('S 'Z) xs
forall {k} (a :: k). a :~: a
Refl
SS Sing n
m -> \case
KList xs
KNil -> Drop ('S m) xs :~: Drop m (Take m xs ++ Drop ('S m) xs)
forall {k} (a :: k). a :~: a
Refl
KCons Proxy x
_ (Proxy xs
Proxy :: Proxy ys) -> SingNat n
-> KList xs
-> Drop ('S n) xs :~: Drop n (Take n xs ++ Drop ('S n) xs)
forall {k} (xs :: [k]) (m :: Nat).
SingNat m
-> KList xs
-> Drop ('S m) xs :~: Drop m (Take m xs ++ Drop ('S m) xs)
lemma2 Sing n
SingNat n
m (forall (l :: [k]). KnownList l => KList l
forall {k} (l :: [k]). KnownList l => KList l
klist @ys)
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