{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
module Michelson.Optimizer
( optimize
, optimizeWithConf
, defaultOptimizerConf
, defaultRules
, defaultRulesAndPushPack
, orRule
, orSimpleRule
, Rule
, OptimizerConf (..)
, ocGotoValuesL
) where
import Prelude hiding (EQ, LT, GT)
import Control.Lens (makeLensesFor)
import Data.Constraint (Dict(..))
import Data.Default (Default(def))
import Data.Singletons (sing)
import Michelson.Interpret.Pack (packValue')
import Michelson.Typed.Aliases (Value)
import Michelson.Typed.Arith
import Michelson.Typed.Instr
import Michelson.Typed.Scope (PackedValScope)
import Michelson.Typed.Sing
import Michelson.Typed.T
import Michelson.Typed.Util (DfsSettings(..), dfsInstr)
import Michelson.Typed.Value
import Util.PeanoNatural
data OptimizerConf = OptimizerConf
{ OptimizerConf -> Bool
ocGotoValues :: Bool
, OptimizerConf -> Rule -> Rule
ocRuleset :: Rule -> Rule
}
defaultOptimizerConf :: OptimizerConf
defaultOptimizerConf :: OptimizerConf
defaultOptimizerConf = OptimizerConf :: Bool -> (Rule -> Rule) -> OptimizerConf
OptimizerConf
{ ocGotoValues :: Bool
ocGotoValues = Bool
True
, ocRuleset :: Rule -> Rule
ocRuleset = Rule -> Rule
defaultRules
}
instance Default OptimizerConf where
def :: OptimizerConf
def = OptimizerConf
defaultOptimizerConf
optimize :: Instr inp out -> Instr inp out
optimize :: 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 :: OptimizerConf -> Instr inp out -> Instr inp out
optimizeWithConf (OptimizerConf Bool
ocGotoValues Rule -> Rule
rules)
= ((Instr inp out, ()) -> Instr inp out
forall a b. (a, b) -> a
fst ((Instr inp out, ()) -> Instr inp out)
-> (Instr inp out -> (Instr inp out, ()))
-> Instr inp out
-> Instr inp out
forall b c a. (b -> c) -> (a -> b) -> a -> c
.)
((Instr inp out -> (Instr inp out, ()))
-> Instr inp out -> Instr inp out)
-> (Instr inp out -> (Instr inp out, ()))
-> Instr inp out
-> Instr inp out
forall a b. (a -> b) -> a -> b
$ DfsSettings ()
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, ()))
-> Instr inp out
-> (Instr inp out, ())
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings ()
dfsSettings
((forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, ()))
-> Instr inp out -> (Instr inp out, ()))
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, ()))
-> Instr inp out
-> (Instr inp out, ())
forall a b. (a -> b) -> a -> b
$ (Instr i o -> (Instr i o, ())
forall a. a -> (a, ())
adapter (Instr i o -> (Instr i o, ()))
-> (Instr i o -> Instr i o) -> Instr i o -> (Instr i o, ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
.)
((Instr i o -> Instr i o) -> Instr i o -> (Instr i o, ()))
-> (Instr i o -> Instr i o) -> Instr i o -> (Instr i o, ())
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 -> Instr i o -> Instr i o) -> Rule -> Instr i o -> Instr i o
forall a b. (a -> b) -> a -> b
$ (Rule -> Rule) -> Rule
fixpoint Rule -> Rule
rules
where
dfsSettings :: DfsSettings ()
dfsSettings = DfsSettings ()
forall a. Default a => a
def{ dsGoToValues :: Bool
dsGoToValues = Bool
ocGotoValues }
type Rule = forall inp out. Instr inp out -> Maybe (Instr inp out)
defaultRules :: Rule -> Rule
defaultRules :: Rule -> Rule
defaultRules =
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
flattenFn
(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
adjacentDips
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
adjacentDrops
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
isSomeOnIf
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
specificPush
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
pairUnpair
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
unpairMisc
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
swapBeforeCommutative
(Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
justDrops
defaultRulesAndPushPack :: Rule -> Rule
defaultRulesAndPushPack :: Rule -> Rule
defaultRulesAndPushPack = Rule -> Rule
defaultRules (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
pushPack
flattenSeqLHS :: Rule -> Rule
flattenSeqLHS :: Rule -> Rule
flattenSeqLHS Rule
toplevel = \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 :: Instr inp out -> Maybe (Instr inp out)
removeNesting = \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 :: Instr inp out -> Maybe (Instr inp out)
removeExtStackType = \case
Ext (STACKTYPE{}) -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (s :: [T]). Instr s s
Nop
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
flattenFn :: Rule
flattenFn :: Instr inp out -> Maybe (Instr inp out)
flattenFn = \case
Fn Text
_ StackFn
_ 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
dipDrop2swapDrop :: Rule
dipDrop2swapDrop :: Instr inp out -> Maybe (Instr inp out)
dipDrop2swapDrop = \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) (s :: [T]). Instr (a : s) s
DROP
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
ifNopNop2Drop :: Rule
ifNopNop2Drop :: Instr inp out -> Maybe (Instr inp out)
ifNopNop2Drop = \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) (s :: [T]). Instr (a : s) s
DROP
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
nopIsNeutralForSeq :: Rule
nopIsNeutralForSeq :: Instr inp out -> Maybe (Instr inp out)
nopIsNeutralForSeq = \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 :: Instr inp out -> Maybe (Instr inp out)
variousNops = \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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
Nop
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
dupSwap2dup :: Rule
dupSwap2dup :: Instr inp out -> Maybe (Instr inp out)
dupSwap2dup = \case
Instr inp b
DUP :# Instr b b
SWAP :# Instr b out
c -> Instr (a : s) out -> Maybe (Instr (a : s) out)
forall a. a -> Maybe a
Just (Instr (a : s) (a : a : s)
forall (a :: T) (s :: [T]).
DupableScope a =>
Instr (a : s) (a : a : s)
DUP Instr (a : s) (a : a : s)
-> Instr (a : a : s) out -> Instr (a : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr (a : a : s) out
c)
Instr inp b
DUP :# Instr b out
SWAP -> Instr (a : s) (a : a : s) -> Maybe (Instr (a : s) (a : a : s))
forall a. a -> Maybe a
Just Instr (a : s) (a : a : s)
forall (a :: T) (s :: [T]).
DupableScope a =>
Instr (a : s) (a : a : s)
DUP
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
noDipNeeded :: Rule
noDipNeeded :: Instr inp out -> Maybe (Instr inp out)
noDipNeeded = \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 (t : c)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr t
x Instr c (t : c) -> Instr (t : c) out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr (t : c) out
c
PUSH Value' Instr t
x :# DIP Instr a c
f -> Instr a (t : c) -> Maybe (Instr a (t : c))
forall a. a -> Maybe a
Just (Instr a (t : c) -> Maybe (Instr a (t : c)))
-> Instr a (t : c) -> Maybe (Instr a (t : c))
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c (t : c) -> Instr a (t : c)
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Value' Instr t -> Instr c (t : c)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
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 ('TUnit : c)
forall (s :: [T]). Instr s ('TUnit : s)
UNIT Instr c ('TUnit : c) -> Instr ('TUnit : c) out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr ('TUnit : c) out
c
Instr inp b
UNIT :# DIP Instr a c
f -> Instr a ('TUnit : c) -> Maybe (Instr a ('TUnit : c))
forall a. a -> Maybe a
Just (Instr a ('TUnit : c) -> Maybe (Instr a ('TUnit : c)))
-> Instr a ('TUnit : c) -> Maybe (Instr a ('TUnit : c))
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c ('TUnit : c) -> Instr a ('TUnit : c)
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c ('TUnit : c)
forall (s :: [T]). Instr s ('TUnit : s)
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 ('TTimestamp : c)
forall (s :: [T]). Instr s ('TTimestamp : s)
NOW Instr c ('TTimestamp : c)
-> Instr ('TTimestamp : c) out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr ('TTimestamp : c) out
c
Instr inp b
NOW :# DIP Instr a c
f -> Instr a ('TTimestamp : c) -> Maybe (Instr a ('TTimestamp : c))
forall a. a -> Maybe a
Just (Instr a ('TTimestamp : c) -> Maybe (Instr a ('TTimestamp : c)))
-> Instr a ('TTimestamp : c) -> Maybe (Instr a ('TTimestamp : c))
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c ('TTimestamp : c) -> Instr a ('TTimestamp : c)
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c ('TTimestamp : c)
forall (s :: [T]). Instr s ('TTimestamp : s)
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 ('TAddress : c)
forall (s :: [T]). Instr s ('TAddress : s)
SENDER Instr c ('TAddress : c) -> Instr ('TAddress : c) out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr ('TAddress : c) out
c
Instr inp b
SENDER :# DIP Instr a c
f -> Instr a ('TAddress : c) -> Maybe (Instr a ('TAddress : c))
forall a. a -> Maybe a
Just (Instr a ('TAddress : c) -> Maybe (Instr a ('TAddress : c)))
-> Instr a ('TAddress : c) -> Maybe (Instr a ('TAddress : c))
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c ('TAddress : c) -> Instr a ('TAddress : c)
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c ('TAddress : c)
forall (s :: [T]). Instr s ('TAddress : s)
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 ('TMap a b : c)
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, SingI b, Comparable a) =>
Instr s ('TMap a b : s)
EMPTY_MAP Instr c ('TMap a b : c) -> Instr ('TMap a b : c) out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr ('TMap a b : c) out
c
Instr inp b
EMPTY_MAP :# DIP Instr a c
f -> Instr a ('TMap a b : c) -> Maybe (Instr a ('TMap a b : c))
forall a. a -> Maybe a
Just (Instr a ('TMap a b : c) -> Maybe (Instr a ('TMap a b : c)))
-> Instr a ('TMap a b : c) -> Maybe (Instr a ('TMap a b : c))
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c ('TMap a b : c) -> Instr a ('TMap a b : c)
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c ('TMap a b : c)
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, SingI b, Comparable a) =>
Instr s ('TMap a b : s)
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 ('TSet e : c)
forall (e :: T) (s :: [T]).
(SingI e, Comparable e) =>
Instr s ('TSet e : s)
EMPTY_SET Instr c ('TSet e : c) -> Instr ('TSet e : c) out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr ('TSet e : c) out
c
Instr inp b
EMPTY_SET :# DIP Instr a c
f -> Instr a ('TSet e : c) -> Maybe (Instr a ('TSet e : c))
forall a. a -> Maybe a
Just (Instr a ('TSet e : c) -> Maybe (Instr a ('TSet e : c)))
-> Instr a ('TSet e : c) -> Maybe (Instr a ('TSet e : c))
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c ('TSet e : c) -> Instr a ('TSet e : c)
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c ('TSet e : c)
forall (e :: T) (s :: [T]).
(SingI e, Comparable e) =>
Instr s ('TSet e : s)
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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 :: Instr inp out -> Maybe (Instr inp out)
branchShortCut = \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 (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 (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 :: Instr inp out -> Maybe (Instr inp out)
compareWithZero = \case
PUSH (VInt Integer
0) :# Instr b b
COMPARE :# Instr b b
EQ :# Instr b out
c -> Instr ('TInt : s) out -> Maybe (Instr ('TInt : s) out)
forall a. a -> Maybe a
Just (Instr ('TInt : s) out -> Maybe (Instr ('TInt : s) out))
-> Instr ('TInt : s) out -> Maybe (Instr ('TInt : s) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TInt : s) b
forall (n :: T) (s :: [T]).
UnaryArithOp Eq' n =>
Instr (n : s) (UnaryArithRes Eq' n : s)
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 (VNat Natural
0) :# Instr b b
COMPARE :# Instr b b
EQ :# Instr b out
c -> Instr ('TNat : s) out -> Maybe (Instr ('TNat : s) out)
forall a. a -> Maybe a
Just (Instr ('TNat : s) out -> Maybe (Instr ('TNat : s) out))
-> Instr ('TNat : s) out -> Maybe (Instr ('TNat : s) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TNat : s) ('TInt : s)
forall (n :: T) (s :: [T]).
ToIntArithOp n =>
Instr (n : s) ('TInt : s)
INT Instr ('TNat : s) ('TInt : s)
-> Instr ('TInt : s) out -> Instr ('TNat : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TInt : s) b
forall (n :: T) (s :: [T]).
UnaryArithOp Eq' n =>
Instr (n : s) (UnaryArithRes Eq' n : s)
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 (n :: T) (s :: [T]).
UnaryArithOp Eq' n =>
Instr (n : s) (UnaryArithRes Eq' n : s)
EQ
PUSH (VNat Natural
0) :# Instr b b
COMPARE :# Instr b out
EQ -> Instr ('TNat : s) out -> Maybe (Instr ('TNat : s) out)
forall a. a -> Maybe a
Just (Instr ('TNat : s) out -> Maybe (Instr ('TNat : s) out))
-> Instr ('TNat : s) out -> Maybe (Instr ('TNat : s) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TNat : s) ('TInt : s)
forall (n :: T) (s :: [T]).
ToIntArithOp n =>
Instr (n : s) ('TInt : s)
INT Instr ('TNat : s) ('TInt : s)
-> Instr ('TInt : s) out -> Instr ('TNat : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TInt : s) out
forall (n :: T) (s :: [T]).
UnaryArithOp Eq' n =>
Instr (n : s) (UnaryArithRes Eq' n : s)
EQ
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
simpleDrops :: Rule
simpleDrops :: Instr inp out -> Maybe (Instr inp out)
simpleDrops = \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 (s :: [T]). Instr s s
Nop
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
internalNop :: Rule
internalNop :: Instr inp out -> Maybe (Instr inp out)
internalNop = \case
DIP Instr a c
Nop -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (s :: [T]). Instr s s
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 :: Instr inp out -> Maybe (Instr inp out)
simpleDips = \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
adjacentDips :: Rule
adjacentDips :: Instr inp out -> Maybe (Instr inp out)
adjacentDips = \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
adjacentDrops :: Rule
adjacentDrops :: Instr inp out -> Maybe (Instr inp out)
adjacentDrops = \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 :: Peano) (s :: [T]).
(RequireLongerOrSameLength s n, NFData (Sing n)) =>
PeanoNatural n -> Instr s (Drop n s)
DROPN PeanoNatural ('S ('S 'Z))
forall (n :: Peano). (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 :: Peano) (s :: [T]).
(RequireLongerOrSameLength s n, NFData (Sing n)) =>
PeanoNatural n -> Instr s (Drop n s)
DROPN PeanoNatural ('S ('S 'Z))
forall (n :: Peano). (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 :: Instr inp out -> Maybe (Instr inp out)
specificPush = \case
push :: Instr inp out
push@PUSH{} -> Instr inp out -> Maybe (Instr inp out)
Rule
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)
Rule
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 :: 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 ('TUnit : inp) -> Maybe (Instr inp ('TUnit : inp))
forall a. a -> Maybe a
Just Instr inp ('TUnit : inp)
forall (s :: [T]). Instr s ('TUnit : s)
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 SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @v of STMap{} -> Instr inp ('TMap k v : inp) -> Maybe (Instr inp ('TMap k v : inp))
forall a. a -> Maybe a
Just Instr inp ('TMap k v : inp)
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, SingI b, Comparable a) =>
Instr s ('TMap a b : s)
EMPTY_MAP
VSet Set (Value' Instr t)
m
| Set (Value' Instr t) -> Bool
forall t. Container t => t -> Bool
null Set (Value' Instr t)
m -> case SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @v of STSet{} -> Instr inp ('TSet t : inp) -> Maybe (Instr inp ('TSet t : inp))
forall a. a -> Maybe a
Just Instr inp ('TSet t : inp)
forall (e :: T) (s :: [T]).
(SingI e, Comparable e) =>
Instr s ('TSet e : s)
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 :: Instr inp out -> Maybe (Instr inp out)
isSomeOnIf = \case
IF (PUSH (VOption Just{})) (PUSH (VOption Maybe (Value' Instr t)
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 (s :: [T]). Instr s s
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 :: Instr inp out -> Maybe (Instr inp out)
pairUnpair = \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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
Nop
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
unpairMisc :: Rule
unpairMisc :: Instr inp out -> Maybe (Instr inp out)
unpairMisc = \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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : b : s)) =>
Instr i o
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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : b : s)) =>
Instr i o
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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : b : s)) =>
Instr i o
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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : b : s)) =>
Instr i o
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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (b : s)) =>
Instr i o
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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (b : s)) =>
Instr i o
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 :: 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 <- ArithOp Add n m =>
Maybe (Dict (ArithRes Add n m ~ ArithRes Add m n, ArithOp Add m n))
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)
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 (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
Instr (n : m : s) out
MUL -> do Dict (ArithRes Mul n m ~ ArithRes Mul m n, ArithOp Mul m n)
Dict <- ArithOp Mul n m =>
Maybe (Dict (ArithRes Mul n m ~ ArithRes Mul m n, ArithOp Mul m n))
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)
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 (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
Instr (n : m : s) out
OR -> do Dict (ArithRes Or n m ~ ArithRes Or m n, ArithOp Or m n)
Dict <- ArithOp Or n m =>
Maybe (Dict (ArithRes Or n m ~ ArithRes Or m n, ArithOp Or m n))
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)
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 (n :: T) (m :: T) (s :: [T]).
ArithOp Or n m =>
Instr (n : m : s) (ArithRes Or n m : s)
OR
Instr (n : m : s) out
AND -> do Dict (ArithRes And n m ~ ArithRes And m n, ArithOp And m n)
Dict <- ArithOp And n m =>
Maybe (Dict (ArithRes And n m ~ ArithRes And m n, ArithOp And m n))
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)
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 (n :: T) (m :: T) (s :: [T]).
ArithOp And n m =>
Instr (n : m : s) (ArithRes And n m : s)
AND
Instr (n : m : s) out
XOR -> do Dict (ArithRes Xor n m ~ ArithRes Xor m n, ArithOp Xor m n)
Dict <- ArithOp Xor n m =>
Maybe (Dict (ArithRes Xor n m ~ ArithRes Xor m n, ArithOp Xor m n))
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)
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 (n :: T) (m :: T) (s :: [T]).
ArithOp Xor n m =>
Instr (n : m : s) (ArithRes Xor n m : s)
XOR
Instr (n : m : s) out
_ -> Maybe (Instr (m : n : s) out)
forall a. Maybe a
Nothing
swapBeforeCommutative :: Rule
swapBeforeCommutative :: Instr inp out -> Maybe (Instr inp out)
swapBeforeCommutative = \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 :: Instr inp out -> Maybe (Instr inp out)
pushPack = \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 :: Value t -> Instr s ('TBytes : s)
pushPacked = Value' Instr 'TBytes -> Instr s ('TBytes : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
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 :: Instr inp out -> Maybe (Instr inp out)
justDrops = \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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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 Notes p
_ 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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
DROP
CONTRACT Notes p
_ 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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
DROP
Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
linearizeAndReapply :: Rule -> Instr inp out -> Instr inp out
linearizeAndReapply :: 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 (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
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 (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
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 Instr inp out
x = Rule -> Instr inp out -> Maybe (Instr inp out)
Rule -> Rule
l Rule
topl Instr inp out
x Maybe (Instr inp out)
-> Maybe (Instr inp out) -> Maybe (Instr inp out)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Rule -> Instr inp out -> Maybe (Instr inp out)
Rule -> Rule
r Rule
topl Instr inp out
x
orSimpleRule :: (Rule -> Rule) -> Rule -> (Rule -> Rule)
orSimpleRule :: (Rule -> Rule) -> Rule -> Rule -> Rule
orSimpleRule Rule -> Rule
l Rule
r Rule
topl Instr inp out
x = Rule -> Instr inp out -> Maybe (Instr inp out)
Rule -> Rule
l Rule
topl Instr inp out
x Maybe (Instr inp out)
-> Maybe (Instr inp out) -> Maybe (Instr inp out)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Instr inp out -> Maybe (Instr inp out)
Rule
r Instr inp out
x
fixpoint :: (Rule -> Rule) -> Rule
fixpoint :: (Rule -> Rule) -> Rule
fixpoint Rule -> Rule
r = Instr inp out -> Maybe (Instr inp out)
Rule
go
where
go :: Rule
go :: Instr inp out -> Maybe (Instr inp out)
go = Rule -> Rule
whileApplies (Rule -> Rule
r Rule
go)
applyOnce :: Rule -> Instr inp out -> Instr inp out
applyOnce :: 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 (Instr inp out -> Maybe (Instr inp out)
Rule
r Instr inp out
i)
adapter :: a -> (a, ())
adapter :: a -> (a, ())
adapter a
a = (a
a, ())
whileApplies :: Rule -> Rule
whileApplies :: Rule -> Rule
whileApplies Rule
r = Instr inp out -> Maybe (Instr inp out)
go
where
go :: 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)
go (Instr inp out -> Maybe (Instr inp out)
Rule
r Instr inp out
i)
makeLensesFor [("ocGotoValues", "ocGotoValuesL")] ''OptimizerConf